let module T = CicTypeChecker in
let module R = CicReduction in
let module C = Cic in
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = max (CicMkImplicit.new_meta metasenv subst) maxmeta in
let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
=
let module C = Cic in
let module R = CicReduction in
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let (context',ty',bo') =
term (proof, goal)
=
let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
+ let curi,metasenv,pbo,pty, attrs = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let newmeta1 = ProofEngineHelpers.new_meta_of_proof ~proof in
let newmeta2 = newmeta1 + 1 in
term (proof, goal)
=
let module C = Cic in
- let curi,metasenv,pbo,pty = proof in
+ let curi,metasenv,pbo,pty, attrs = proof in
(* occur check *)
let occur i t =
let m = CicUtil.metas_of_term t in
let exact_tac ~term =
let exact_tac ~term (proof, goal) =
(* Assumption: the term bo must be closed in the current context *)
- let (_,metasenv,_,_) = proof in
+ let (_,metasenv,_,_, _) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let module T = CicTypeChecker in
let module R = CicReduction in
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let (curi,metasenv,proofbo,proofty) = proof in
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',proofbo,proofty in
+ let proof' = curi,metasenv'',proofbo,proofty, attrs in
let proof'', new_goals' =
apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_,_) = proof'' in
+ let (_,metasenv''',_,_, _) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
) new_goals @ new_goals'
let module U = UriManager in
let module R = CicReduction in
let module C = Cic in
- let (curi,metasenv,proofbo,proofty) = proof in
+ let (curi,metasenv,proofbo,proofty, attrs) = proof in
let metano,context,ty = CicUtil.lookup_meta goal metasenv in
let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
let termty = CicReduction.whd context termty in
let term_to_refine =
C.MutCase (uri,typeno,outtype,term,patterns)
in
-prerr_endline (CicMetaSubst.ppterm_in_context ~metasenv:metasenv' [] term_to_refine context);
let refined_term,_,metasenv'',_ =
CicRefine.type_of_aux' metasenv' context term_to_refine
CicUniv.empty_ugraph
ProofEngineHelpers.compare_metasenvs
~oldmetasenv:metasenv ~newmetasenv:metasenv''
in
- let proof' = curi,metasenv'',proofbo,proofty in
+ let proof' = curi,metasenv'',proofbo,proofty, attrs in
let proof'', new_goals' =
apply_tactic (apply_tac ~term:refined_term) (proof',goal)
in
(* The apply_tactic can have closed some of the new_goals *)
let patched_new_goals =
- let (_,metasenv''',_,_) = proof'' in
+ let (_,metasenv''',_,_,_) = proof'' in
List.filter
(function i -> List.exists (function (j,_,_) -> j=i) metasenv'''
) new_goals @ new_goals'
let mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[] in
let term = C.Sort C.Set in
let letout_tac (proof, goal) =
- let curi, metasenv, pbo, pty = proof in
+ let curi, metasenv, pbo, pty, attrs = proof in
let metano, context, ty = CicUtil.lookup_meta goal metasenv in
let newmeta = ProofEngineHelpers.new_meta_of_proof ~proof in
let fresh_name = mk_fresh_name_callback metasenv context (Cic.Name "hole") ~typ:term in