- let t',metasenv',subst' =
- try
- CicMetaSubst.delift n subst context metasenv l t
- with
- (CicMetaSubst.MetaSubstFailure msg)-> raise(UnificationFailure msg)
- | (CicMetaSubst.Uncertain msg) -> raise (Uncertain msg)
- in
- let t'' =
- 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
- ignore (CicUniv.add_ge (upper u u') (lower u u')) ;
- s
- | _ -> t'
- in
- (n, t'')::subst', metasenv'
- in
- 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)
- *)
+ (* First of all we unify the type of the meta with the type of the term *)
+ let subst,metasenv =
+ 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)
+ *)