let profiler4 = HExtlib.profile "P/Inference.unif_simple[filter]"
let unification_aux b metasenv1 metasenv2 context t1 t2 ugraph =
- let metasenv = metasenv1 @ metasenv2 in
+ let metasenv =
+ HExtlib.list_uniq (List.sort Pervasives.compare (metasenv1 @ metasenv2))
+ (*metasenv1 @ metasenv2*)
+ in
let subst, menv, ug =
if not (is_simple_term t1) || not (is_simple_term t2) then (
debug_print