+ try
+(*assert (try n = -1 or (ignore(NCicUtils.lookup_meta n metasenv); true) with NCicUtils.Meta_not_found _ -> false);*)
+ let ((metasenv,subst),t) as res = aux (context,0,0) (metasenv,subst) t in
+ if (try n <> -1 && (ignore(NCicUtils.lookup_meta n metasenv); false)
+ with NCicUtils.Meta_not_found _ -> true)
+ then
+ let _,context,bo,_ = NCicUtils.lookup_subst n subst in
+ match unify metasenv subst context bo t with
+ None -> raise (NotFound `NotWellTyped)
+ | Some (metasenv,subst) -> (metasenv,subst),t
+ else
+ (try
+ let _,context,ty = NCicUtils.lookup_meta n metasenv in
+ let ty' =
+ match t with
+ NCic.Sort _ -> (* could be algebraic *) NCic.Implicit `Closed
+ | _ -> NCicTypeChecker.typeof status ~subst ~metasenv context t in
+ (match ty,ty' with
+ NCic.Implicit _,_ ->
+ (match ty' with
+ NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
+ | _ -> raise TypeNotGood)
+ | _,NCic.Implicit _ ->
+ (match ty with
+ NCic.Sort _ | NCic.Meta _ | NCic.Implicit _ -> res
+ | _ -> raise TypeNotGood)
+ | _ ->
+ if
+ NCicReduction.are_convertible status ~metasenv ~subst context ty' ty
+ then
+ res
+ else
+ raise TypeNotGood)
+ with
+ NCicUtils.Meta_not_found _ ->
+ (* Fake metavariable used in NTacStatus and NCicRefiner :-( *)
+ assert (n = -1); res
+ | NCicTypeChecker.TypeCheckerFailure msg ->
+ HLog.error "----------- Problem with Dependent Types ----------";
+ HLog.error (Lazy.force msg) ;
+ HLog.error "---------------------------------------------------";
+ raise (NotFound `NotWellTyped)
+ | TypeNotGood
+ | NCicTypeChecker.AssertFailure _
+ | NCicReduction.AssertFailure _
+ | NCicTypeChecker.TypeCheckerFailure _ ->
+ raise (NotFound `NotWellTyped))
+ with NotFound reason ->