- 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