if swap then unify test_eq_only m s c t2 t1
else unify test_eq_only m s c t1 t2
in
- let ty_t =
- try NCicTypeChecker.typeof ~subst ~metasenv context t
- with NCicTypeChecker.TypeCheckerFailure msg ->
- prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
- prerr_endline (Lazy.force msg);
- assert false
- in
let name, ctx, ty = NCicUtils.lookup_meta n metasenv in
- let lty = NCicSubstitution.subst_meta lc ty in
- pp (lazy("On the types: " ^
- NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
- ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
- let metasenv, subst = unify test_eq_only metasenv subst context lty ty_t in
+ let metasenv, subst =
+ match ty with
+ | NCic.Implicit (`Typeof _) -> metasenv, subst
+ | _ ->
+ let lty = NCicSubstitution.subst_meta lc ty in
+ let ty_t =
+ try NCicTypeChecker.typeof ~subst ~metasenv context t
+ with NCicTypeChecker.TypeCheckerFailure msg ->
+ prerr_endline (NCicPp.ppterm ~metasenv ~subst ~context t);
+ prerr_endline (Lazy.force msg);
+ assert false
+ in
+ pp (lazy("On the types: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context lty ^ " === "
+ ^ NCicPp.ppterm ~metasenv ~subst ~context ty_t));
+ unify test_eq_only metasenv subst context lty ty_t
+ in
let (metasenv, subst), t =
try NCicMetaSubst.delift metasenv subst context n lc t
with NCicMetaSubst.Uncertain msg -> raise (Uncertain msg)
try
let _, _,oldt,_ = NCicUtils.lookup_subst n subst in
let oldt = NCicSubstitution.subst_meta lc oldt in
+ let t = NCicSubstitution.subst_meta lc t in
(* conjecture: always fail --> occur check *)
unify test_eq_only metasenv subst context oldt t
with NCicUtils.Subst_not_found _ ->
* we could ? := Type_j with j <= i... *)
let subst = (n, (name, ctx, t, ty)) :: subst in
pp (lazy ("?"^string_of_int n^" := "^NCicPp.ppterm
- ~metasenv ~subst ~context:ctx (NCicSubstitution.subst_meta lc t)));
+ ~metasenv ~subst ~context (NCicSubstitution.subst_meta lc t)));
let metasenv =
List.filter (fun (m,_) -> not (n = m)) metasenv
in