;;
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 ->