(* Note: this code is almost identical to change_tac and
* it could be unified by making the change function a callback *)
let reduction_tac ~reduction ~pattern (proof,goal) =
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+ ProofEngineHelpers.select ~subst ~metasenv ~ugraph:CicUniv.oblivion_ugraph
~conjecture ~pattern
in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
| _ as t -> t
) metasenv
in
- (curi,metasenv',_subst,pbo,pty, attrs), [metano]
+ (curi,metasenv',subst,pbo,pty, attrs), [metano]
;;
let simpl_tac ~pattern =
term(s) to be replaced. *)
let change_tac ?(with_cast=false) ~pattern with_what =
let change_tac ~pattern ~with_what (proof, goal) =
- let curi,metasenv,_subst,pbo,pty, attrs = proof in
+ let curi,metasenv,subst,pbo,pty, attrs = proof in
let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
let change subst where terms metasenv ugraph =
if terms = [] then where, metasenv, ugraph
with_what context_of_t metasenv ugraph
in
let _,u =
- CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
+ CicTypeChecker.type_of_aux'
+ metasenv ~subst context_of_t with_what ugraph
in
let b,_ =
- CicReduction.are_convertible ~metasenv context_of_t t with_what u
+ CicReduction.are_convertible
+ ~metasenv ~subst context_of_t t with_what u
in
if b then
((t, with_what) :: pairs), metasenv, ugraph
CicMetaSubst.apply_subst subst where', metasenv, ugraph
in
let (subst,metasenv,ugraph,selected_context,selected_ty) =
- ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
- ~pattern in
+ ProofEngineHelpers.select
+ ~metasenv ~subst ~ugraph:CicUniv.oblivion_ugraph ~conjecture ~pattern
+ in
let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
let context', metasenv, ugraph =
List.fold_right2
| _ as t -> t)
metasenv
in
- let proof,goal = (curi,metasenv',_subst,pbo,pty, attrs), metano in
+ let proof,goal = (curi,metasenv',subst,pbo,pty, attrs), metano in
if with_cast then
let metano' = ProofEngineHelpers.new_meta_of_proof ~proof in
let (newproof,_) =
proof,[goal]
in
mk_tactic (change_tac ~pattern ~with_what)
+;;
let fold_tac ~reduction ~term ~pattern =
let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
(change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
in
mk_tactic (fold_tac ~reduction ~term ~pattern)
+;;