- let (_,_,meta_type) =
- List.find (function (m,_,_) -> m=n) metasenv' in
- let tyt = type_of_aux' metasenv' subst' context t in
- fo_unif_subst subst' context metasenv' (S.lift_meta l meta_type) tyt
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv' in
+ (try
+ let tyt =
+ type_of_aux' metasenv' subst'' context t
+ in
+ fo_unif_subst
+ test_equality_only
+ subst'' context metasenv' tyt (S.lift_meta l meta_type)
+ with AssertFailure _ ->
+ (* TODO huge hack!!!!
+ * we keep on unifying/refining in the hope that the problem will be
+ * eventually solved. In the meantime we're breaking a big invariant:
+ * the terms that we are unifying are no longer well typed in the
+ * current context (in the worst case we could even diverge)
+ *)
+(*
+prerr_endline "********* FROM NOW ON EVERY REASONABLE INVARIANT IS BROKEN.";
+prerr_endline "********* PROCEED AT YOUR OWN RISK. AND GOOD LUCK." ;
+*)
+ (subst'', metasenv'))