if Utils.debug_metas then
ignore(check_for_duplicates menv "unification_aux prima di apply_subst");
let menv = Subst.apply_subst_metasenv subst menv in
- let _ = check_for_duplicates menv "unif_aux after" in
- check_metasenv "unification_aux after 1" menv;
- subst, menv, ug
+ if Utils.debug_metas then
+ (let _ = check_for_duplicates menv "unif_aux after" in
+ check_metasenv "unification_aux after 1" menv);
+ subst, menv, ug
;;
exception MatchingFailure;;
;;
let unification m1 m2 c t1 t2 ug =
+ let m1 =
+ if (m1 = m2 && m1 <> []) then assert false
+ (* (prerr_endline "eccoci 2"; []) *) else m1 in
+ (*
+ prerr_endline (CicPp.ppterm t1);
+ prerr_endline (CicPp.ppterm t2);
+ prerr_endline "++++++++++"; *)
try
unification_aux true m1 m2 c t1 t2 ug
with exn ->