Commit caf8cdf2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

Term.compare: cannot use physical equality on terms with deferred substitution

parent 004f0edf
......@@ -337,7 +337,7 @@ let t_compare t1 t2 =
| Por _, _ -> raise CompLT | _, Por _ -> raise CompGT
in
let rec t_compare bnd vml1 vml2 t1 t2 =
if t1 != t2 then begin
if t1 != t2 || vml1 <> [] || vml2 <> [] then begin
oty_compare t1.t_ty t2.t_ty;
comp_raise (Slab.compare t1.t_label t2.t_label);
match descend vml1 t1, descend vml2 t2 with
......
Supports Markdown
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