Commit d53ca3c7 by Kim Nguyễn

Remove the `variable kind` heuristics introduced by commit:dd209d29.

parent 6018a66f
......@@ -753,8 +753,6 @@ let apply_raw delta s t =
);
NormMemoHash.clear memo_norm;
let s = Substitution.kind delta Var.function_kind s in
let t = Substitution.kind delta Var.argument_kind t in
let vgamma = Var.mk "Gamma" in
let gamma = var vgamma in
let cgamma = cons gamma in
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment