let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
let (consthead,newmetasenv,arguments,_) =
let subst,newmetasenv',_ =
CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
in
let subst,newmetasenv',_ =
CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
in
Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
| _ -> 0
(* 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
(* 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 exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
match term with
C.Var (uri,exp_named_subst) ->
CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
in
let (newproof, newmetasenv''') =
CicMetaSubst.apply_subst ((metano,(context,bo',Cic.Implicit None))::subst)
in
let (newproof, newmetasenv''') =
- (((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)
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)
(CicMetaSubst.apply_subst subst), status
let apply_tac ~term status = snd (apply_tac_verbose ~term status)
let module R = CicReduction in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module R = CicReduction in
let (_,metasenv,_,_) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module C = Cic in
let curi,metasenv,pbo,pty = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta2 = newmeta1 + 1 in
let fresh_name =
mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
let newmeta2 = newmeta1 + 1 in
let fresh_name =
mk_fresh_name_callback metasenv context (Cic.Name "Hcut") ~typ:term in
[newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
in
(newproof, [newmeta1 ; newmeta2])
[newmeta2,context,term; newmeta1,context_for_newmeta1,newmeta1ty];
in
(newproof, [newmeta1 ; newmeta2])
"You can't letin a term containing the current goal"));
let _,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
"You can't letin a term containing the current goal"));
let _,_ =
CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let newmetaty = CicSubstitution.lift 1 ty in
let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
let (newproof, _) =
let newmetaty = CicSubstitution.lift 1 ty in
let bo' = C.LetIn (fresh_name,term,C.Meta (newmeta,irl)) in
let (newproof, _) =
let letout_tac (proof, goal) =
let curi, metasenv, pbo, pty = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in
let letout_tac (proof, goal) =
let curi, metasenv, pbo, pty = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in
let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
let context_for_newmeta = None :: context in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
let newmetaty = CicSubstitution.lift 1 ty in
let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in
let context_for_newmeta = None :: context in
let irl = CicMkImplicit.identity_relocation_list_for_metavariable context_for_newmeta in
let newmetaty = CicSubstitution.lift 1 ty in
let bo' = C.LetIn (fresh_name, term, C.Meta (newmeta,irl)) in
- let newproof, _ = subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in
+ let newproof, _ = ProofEngineHelpers.subst_meta_in_proof proof metano bo'[newmeta,context_for_newmeta,newmetaty] in