Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
-let apply_with_subst ~term ~subst (proof, goal) =
+let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
(* Assumption: The term "term" must be closed in the current context *)
let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
- let newmeta = CicMkImplicit.new_meta metasenv subst in
+ let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
try
new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
termty n
- with CicUnification.UnificationFailure _ when n > 0 ->
+ with (CicUnification.UnificationFailure _
+ | CicUniv.UniverseInconsistency _ ) when n > 0 ->
add_one_argument (n - 1)
in
add_one_argument goal_arity
ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
newmetasenv''
in
- (((metano,(context,bo',Cic.Implicit None))::subst)(* subst_in *), (* ALB *)
- (newproof,
- List.map (function (i,_,_) -> i) new_uninstantiatedmetas))
+ let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+ subst,
+ (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
+ max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)
(* ALB *)
-let apply_with_subst ~term ?(subst=[]) status =
+let apply_with_subst ~term ?(subst=[]) ?(maxmeta=0) status =
try
(* apply_tac_verbose ~term status *)
- apply_with_subst ~term ~subst status
+ apply_with_subst ~term ~subst ~maxmeta status
(* TODO cacciare anche altre eccezioni? *)
with
| CicUnification.UnificationFailure msg
- | CicTypeChecker.TypeCheckerFailure msg ->
- raise (Fail msg)
+ | CicTypeChecker.TypeCheckerFailure msg -> raise (Fail msg)
+ | CicUniv.UniverseInconsistency msg -> raise (Fail (lazy msg))
(* ALB *)
let apply_tac_verbose ~term status =
- let subst, status = apply_with_subst ~term status in
+ let subst, status, _ = apply_with_subst ~term status in
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)