+(*
+ begin
+ try
+ let (_, oldt) = CicMetaSubst.lookup_subst n subst in
+ let lifted_oldt = S.lift_meta l oldt in
+ let ty_lifted_oldt,ugraph1 =
+ type_of_aux' metasenv subst context lifted_oldt ugraph
+ in
+ let tyt,ugraph2 = type_of_aux' metasenv subst context t ugraph1 in
+ let (subst, metasenv, ugraph3) =
+ fo_unif_subst_ordered test_equality_only subst context metasenv
+ tyt ty_lifted_oldt ugraph2
+ in
+ fo_unif_subst_ordered
+ test_equality_only subst context metasenv t lifted_oldt ugraph3
+ with CicMetaSubst.SubstNotFound _ ->
+ (* First of all we unify the type of the meta with the type of the term *)
+ let subst,metasenv,ugraph1 =
+ let (_,_,meta_type) = CicUtil.lookup_meta n metasenv in
+ (try
+ let tyt,ugraph1 = type_of_aux' metasenv subst context t ugraph in
+ fo_unif_subst
+ test_equality_only
+ subst context metasenv tyt (S.lift_meta l meta_type) ugraph1
+ 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,ugraph))
+ in
+ let t',metasenv,subst =
+ try
+ (* TASSI: I hope delift does nothing with universes *)
+ CicMetaSubst.delift n subst context metasenv l t
+ with
+ (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
+ | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
+ in
+ let t'',ugraph2 =
+ match t' with
+ C.Sort (C.Type u) when not test_equality_only ->
+ let u' = CicUniv.fresh () in
+ let s = C.Sort (C.Type u') in
+ let ugraph2 =
+ CicUniv.add_ge (upper u u') (lower u u') ugraph1 in
+ s,ugraph2
+ | _ -> t',ugraph1
+ in
+ (* Unifying the types may have already instantiated n. Let's check *)
+ try
+ let (_, oldt) = CicMetaSubst.lookup_subst n subst in
+ let lifted_oldt = S.lift_meta l oldt in
+ fo_unif_subst_ordered
+ test_equality_only subst context metasenv t lifted_oldt ugraph2
+ with
+ CicMetaSubst.SubstNotFound _ ->
+ let (_, context, _) = CicUtil.lookup_meta n metasenv in
+ let subst = (n, (context, t'')) :: subst in
+ let metasenv =
+(* CicMetaSubst.apply_subst_metasenv [n,(context, t'')] metasenv *)
+ CicMetaSubst.apply_subst_metasenv subst metasenv
+ in
+ subst, metasenv,ugraph2
+(* (n,t'')::subst, metasenv *)
+ end
+*)