+ let metasenv, subst, t =
+ match ty with
+ | NCic.Implicit (`Typeof _) ->
+ metasenv,subst,fix_sorts swap metasenv subst context (NCic.Meta(n,lc)) t
+ | _ ->
+ pp (lazy ("typeof: " ^ NCicPp.ppterm ~metasenv ~subst ~context t));
+ let t, ty_t =
+ try t, NCicTypeChecker.typeof ~subst ~metasenv context t
+ with NCicTypeChecker.TypeCheckerFailure _ ->
+ let ft =
+ fix_sorts swap metasenv subst context (NCic.Meta (n,lc)) t
+ in
+ if ft == t then assert false
+ else
+ try
+ pp (lazy ("typeof: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context ft));
+ ft, NCicTypeChecker.typeof ~subst ~metasenv context ft
+ with NCicTypeChecker.TypeCheckerFailure _ ->
+ assert false
+ in
+ let lty = NCicSubstitution.subst_meta lc ty in
+ pp (lazy("On the types: " ^
+ NCicPp.ppterm ~metasenv ~subst ~context:ctx ty ^ " ~~~ " ^
+ 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
+ metasenv, subst, t
+ in