aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/class_tactics.ml441
-rw-r--r--tactics/elimschemes.ml24
-rw-r--r--tactics/eqschemes.ml29
-rw-r--r--tactics/eqschemes.mli6
-rw-r--r--tactics/equality.ml49
-rw-r--r--tactics/extratactics.ml410
-rw-r--r--tactics/leminv.ml9
-rw-r--r--tactics/rewrite.ml445
-rw-r--r--tactics/tacinterp.ml8
-rw-r--r--tactics/tactics.ml9
-rw-r--r--tactics/tactics.mli3
12 files changed, 136 insertions, 99 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index fab324962b..29eb9e9ec8 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -983,7 +983,7 @@ let pr_applicable_hint () =
match glss.Evd.it with
| [] -> Errors.error "No focused goal."
| g::_ ->
- let gl = { Evd.it = g; sigma = glss.Evd.sigma } in
+ let gl = { Evd.it = g; sigma = glss.Evd.sigma; eff = Declareops.no_seff } in
pr_hint_term (pf_concl gl)
(* displays the whole hint database db *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index bfe80d7087..21678c9714 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -291,15 +291,16 @@ let make_autogoal_hints =
unfreeze (Some (only_classes, sign, hints)); hints
let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac =
- { skft = fun sk fk {it = gl,hints; sigma=s} ->
- let res = try Some (tac {it=gl; sigma=s}) with e when catchable e -> None in
+ { skft = fun sk fk {it = gl,hints; sigma=s;eff=eff} ->
+ let res = try Some (tac {it=gl; sigma=s;eff=eff})
+ with e when catchable e -> None in
match res with
| Some gls -> sk (f gls hints) fk
| None -> fk () }
let intro_tac : atac =
lift_tactic Tactics.intro
- (fun {it = gls; sigma = s} info ->
+ (fun {it = gls; sigma = s;eff=eff} info ->
let gls' =
List.map (fun g' ->
let env = Goal.V82.env s g' in
@@ -308,13 +309,13 @@ let intro_tac : atac =
(true,false,false) info.only_classes None (List.hd context) in
let ldb = Hint_db.add_list hint info.hints in
(g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls
- in {it = gls'; sigma = s})
+ in {it = gls'; sigma = s;eff=eff})
let normevars_tac : atac =
- { skft = fun sk fk {it = (gl, info); sigma = s} ->
+ { skft = fun sk fk {it = (gl, info); sigma = s; eff=eff} ->
let gl', sigma' = Goal.V82.nf_evar s gl in
let info' = { info with auto_last_tac = lazy (str"normevars") } in
- sk {it = [gl', info']; sigma = sigma'} fk }
+ sk {it = [gl', info']; sigma = sigma';eff=eff} fk }
(* Ordering of states is lexicographic on the number of remaining goals. *)
let compare (pri, _, _, res) (pri', _, _, res') =
@@ -329,9 +330,9 @@ let or_tac (x : 'a tac) (y : 'a tac) : 'a tac =
{ skft = fun sk fk gls -> x.skft sk (fun () -> y.skft sk fk gls) gls }
let hints_tac hints =
- { skft = fun sk fk {it = gl,info; sigma = s} ->
+ { skft = fun sk fk {it = gl,info; sigma = s;eff=eff} ->
let concl = Goal.V82.concl s gl in
- let tacgl = {it = gl; sigma = s} in
+ let tacgl = {it = gl; sigma = s;eff=eff} in
let poss = e_possible_resolve hints info.hints concl in
let rec aux i foundone = function
| (tac, _, b, name, pp) :: tl ->
@@ -343,7 +344,7 @@ let hints_tac hints =
in
(match res with
| None -> aux i foundone tl
- | Some {it = gls; sigma = s'} ->
+ | Some {it = gls; sigma = s';eff=eff} ->
if !typeclasses_debug then
msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
++ str" on" ++ spc () ++ pr_ev s gl);
@@ -375,11 +376,11 @@ let hints_tac hints =
hints =
if b && not (Environ.eq_named_context_val (Goal.V82.hyps s' g) (Goal.V82.hyps s' gl))
then make_autogoal_hints info.only_classes
- ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s'}
+ ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';eff=eff}
else info.hints;
auto_cut = derivs }
in g, info) 1 newgls in
- let glsv = {it = gls'; sigma = s'} in
+ let glsv = {it = gls'; sigma = s';eff=eff} in
sk glsv fk)
| [] ->
if not foundone && !typeclasses_debug then
@@ -422,14 +423,14 @@ let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk
fk)
else fk'
in aux s' (gls'::acc) fk'' gls)
- fk {it = (gl,info); sigma = s})
+ fk {it = (gl,info); sigma = s; eff = Declareops.no_seff })
| [] -> Somek2 (List.rev acc, s, fk)
- in fun {it = gls; sigma = s} fk ->
+ in fun {it = gls; sigma = s; eff = eff} fk ->
let rec aux' = function
| Nonek2 -> fk ()
| Somek2 (res, s', fk') ->
let goals' = List.concat res in
- sk {it = goals'; sigma = s'} (fun () -> aux' (fk' ()))
+ sk {it = goals'; sigma = s'; eff = eff } (fun () -> aux' (fk' ()))
in aux' (aux s [] (fun () -> Nonek2) gls)
let then_tac (first : atac) (second : atac) : atac =
@@ -468,8 +469,8 @@ let cut_of_hints h =
let make_autogoals ?(only_classes=true) ?(st=full_transparent_state) hints gs evm' =
let cut = cut_of_hints hints in
{ it = List.map_i (fun i g ->
- let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'} in
- (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm' }
+ let (gl, auto) = make_autogoal ~only_classes ~st cut (Some (fst g)) {it = snd g; sigma = evm'; eff = Declareops.no_seff } in
+ (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; eff = Declareops.no_seff }
let get_result r =
match r with
@@ -494,11 +495,11 @@ let eauto_tac ?limit hints =
| Some limit -> fix_limit limit (eauto_tac hints)
let eauto ?(only_classes=true) ?st ?limit hints g =
- let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g } in
+ let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; eff=g.eff } in
match run_tac (eauto_tac ?limit hints) gl with
| None -> raise Not_found
- | Some {it = goals; sigma = s} ->
- {it = List.map fst goals; sigma = s}
+ | Some {it = goals; sigma = s; eff=eff} ->
+ {it = List.map fst goals; sigma = s; eff=eff}
let real_eauto st ?limit hints p evd =
let rec aux evd fails =
@@ -544,7 +545,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
let nc, gl, subst, _ = Evarutil.push_rel_context_to_named_context env gl in
let (gl,t,sigma) =
Goal.V82.mk_goal sigma nc gl Store.empty in
- let gls = { it = gl ; sigma = sigma } in
+ let gls = { it = gl ; sigma = sigma; eff= Declareops.no_seff } in (* XXX eff *)
let hints = searchtable_map typeclasses_db in
let gls' = eauto ?limit:!typeclasses_depth ~st:(Hint_db.transparent_state hints) [hints] gls in
let evd = sig_sig gls' in
diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml
index 62d13c0a65..9c020930c8 100644
--- a/tactics/elimschemes.ml
+++ b/tactics/elimschemes.ml
@@ -27,7 +27,7 @@ let optimize_non_type_induction_scheme kind dep sort ind =
(* in case the inductive has a type elimination, generates only one
induction scheme, the other ones share the same code with the
apropriate type *)
- let cte = find_scheme kind ind in
+ let cte, eff = find_scheme kind ind in
let c = mkConst cte in
let t = type_of_constant (Global.env()) cte in
let (mib,mip) = Global.lookup_inductive ind in
@@ -39,24 +39,24 @@ let optimize_non_type_induction_scheme kind dep sort ind =
mib.mind_nparams_rec
else
mib.mind_nparams in
- snd (weaken_sort_scheme (new_sort_in_family sort) npars c t)
+ snd (weaken_sort_scheme (new_sort_in_family sort) npars c t), eff
else
- build_induction_scheme (Global.env()) Evd.empty ind dep sort
+ build_induction_scheme (Global.env()) Evd.empty ind dep sort, Declareops.no_seff
let build_induction_scheme_in_type dep sort ind =
build_induction_scheme (Global.env()) Evd.empty ind dep sort
let rect_scheme_kind_from_type =
declare_individual_scheme_object "_rect_nodep"
- (build_induction_scheme_in_type false InType)
+ (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
let rect_scheme_kind_from_prop =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
- (build_induction_scheme_in_type false InType)
+ (fun x -> build_induction_scheme_in_type false InType x, Declareops.no_seff)
let rect_dep_scheme_kind_from_type =
declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
- (build_induction_scheme_in_type true InType)
+ (fun x -> build_induction_scheme_in_type true InType x, Declareops.no_seff)
let ind_scheme_kind_from_type =
declare_individual_scheme_object "_ind_nodep"
@@ -85,24 +85,24 @@ let build_case_analysis_scheme_in_type dep sort ind =
let case_scheme_kind_from_type =
declare_individual_scheme_object "_case_nodep"
- (build_case_analysis_scheme_in_type false InType)
+ (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
let case_scheme_kind_from_prop =
declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
- (build_case_analysis_scheme_in_type false InType)
+ (fun x -> build_case_analysis_scheme_in_type false InType x, Declareops.no_seff)
let case_dep_scheme_kind_from_type =
declare_individual_scheme_object "_case" ~aux:"_case_from_type"
- (build_case_analysis_scheme_in_type true InType)
+ (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
let case_dep_scheme_kind_from_type_in_prop =
declare_individual_scheme_object "_casep_dep"
- (build_case_analysis_scheme_in_type true InProp)
+ (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
let case_dep_scheme_kind_from_prop =
declare_individual_scheme_object "_case_dep"
- (build_case_analysis_scheme_in_type true InType)
+ (fun x -> build_case_analysis_scheme_in_type true InType x, Declareops.no_seff)
let case_dep_scheme_kind_from_prop_in_prop =
declare_individual_scheme_object "_casep"
- (build_case_analysis_scheme_in_type true InProp)
+ (fun x -> build_case_analysis_scheme_in_type true InProp x, Declareops.no_seff)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index cc11621681..7aac37d1b2 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -180,7 +180,7 @@ let build_sym_scheme env ind =
let sym_scheme_kind =
declare_individual_scheme_object "_sym_internal"
- (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind)
+ (fun ind -> build_sym_scheme (Global.env() (* side-effect! *)) ind, Declareops.no_seff)
(**********************************************************************)
(* Build the involutivity of symmetry for an inductive type *)
@@ -201,7 +201,8 @@ let sym_scheme_kind =
let build_sym_involutive_scheme env ind =
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env ind in
- let sym = mkConst (find_scheme sym_scheme_kind ind) in
+ let c, eff = find_scheme sym_scheme_kind ind in
+ let sym = mkConst c in
let (eq,eqrefl) = get_coq_eq () in
let cstr n = mkApp (mkConstruct(ind,1),extended_rel_vect n paramsctxt) in
let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
@@ -236,7 +237,8 @@ let build_sym_involutive_scheme env ind =
[|mkRel 1|]])|]]);
mkRel 1|])),
mkRel 1 (* varH *),
- [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|]))))
+ [|mkApp(eqrefl,[|applied_ind_C;cstr (nrealargs+1)|])|])))),
+ eff
let sym_involutive_scheme_kind =
declare_individual_scheme_object "_sym_involutive"
@@ -305,8 +307,10 @@ let sym_involutive_scheme_kind =
let build_l2r_rew_scheme dep env ind kind =
let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
get_sym_eq_data env ind in
- let sym = mkConst (find_scheme sym_scheme_kind ind) in
- let sym_involutive = mkConst (find_scheme sym_involutive_scheme_kind ind) in
+ let c, eff = find_scheme sym_scheme_kind ind in
+ let sym = mkConst c in
+ let c, eff' = find_scheme sym_involutive_scheme_kind ind in
+ let sym_involutive = mkConst c in
let (eq,eqrefl) = get_coq_eq () in
let cstr n p =
mkApp (mkConstruct(ind,1),
@@ -384,7 +388,8 @@ let build_l2r_rew_scheme dep env ind kind =
Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
[|main_body|])
else
- main_body))))))
+ main_body)))))),
+ Declareops.union_side_effects eff' eff
(**********************************************************************)
(* Build the left-to-right rewriting lemma for hypotheses associated *)
@@ -613,7 +618,7 @@ let rew_l2r_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_dep_scheme_kind =
declare_individual_scheme_object "_rew_dep"
- (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType)
+ (fun ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
(**********************************************************************)
(* Dependent rewrite from right-to-left in hypotheses *)
@@ -623,7 +628,7 @@ let rew_r2l_dep_scheme_kind =
(**********************************************************************)
let rew_r2l_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_dep"
- (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType)
+ (fun ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
(**********************************************************************)
(* Dependent rewrite from left-to-right in hypotheses *)
@@ -633,7 +638,7 @@ let rew_r2l_forward_dep_scheme_kind =
(**********************************************************************)
let rew_l2r_forward_dep_scheme_kind =
declare_individual_scheme_object "_rew_fwd_r_dep"
- (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType)
+ (fun ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Declareops.no_seff)
(**********************************************************************)
(* Non-dependent rewrite from either left-to-right in conclusion or *)
@@ -647,7 +652,7 @@ let rew_l2r_forward_dep_scheme_kind =
let rew_l2r_scheme_kind =
declare_individual_scheme_object "_rew_r"
(fun ind -> fix_r2l_forward_rew_scheme
- (build_r2l_forward_rew_scheme false (Global.env()) ind InType))
+ (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Declareops.no_seff)
(**********************************************************************)
(* Non-dependent rewrite from either right-to-left in conclusion or *)
@@ -657,7 +662,7 @@ let rew_l2r_scheme_kind =
(**********************************************************************)
let rew_r2l_scheme_kind =
declare_individual_scheme_object "_rew"
- (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType)
+ (fun ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Declareops.no_seff)
(* End of rewriting schemes *)
@@ -728,4 +733,4 @@ let build_congr env (eq,refl) ind =
let congr_scheme_kind = declare_individual_scheme_object "_congr"
(fun ind ->
(* May fail if equality is not defined *)
- build_congr (Global.env()) (get_coq_eq ()) ind)
+ build_congr (Global.env()) (get_coq_eq ()) ind, Declareops.no_seff)
diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli
index 31a96e6dce..72412d12dc 100644
--- a/tactics/eqschemes.mli
+++ b/tactics/eqschemes.mli
@@ -23,7 +23,8 @@ val rew_r2l_dep_scheme_kind : individual scheme_kind
val rew_r2l_scheme_kind : individual scheme_kind
val build_r2l_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
-val build_l2r_rew_scheme : bool -> env -> inductive -> sorts_family -> constr
+val build_l2r_rew_scheme :
+ bool -> env -> inductive -> sorts_family -> constr * Declareops.side_effects
val build_r2l_forward_rew_scheme :
bool -> env -> inductive -> sorts_family -> constr
val build_l2r_forward_rew_scheme :
@@ -34,7 +35,8 @@ val build_l2r_forward_rew_scheme :
val build_sym_scheme : env -> inductive -> constr
val sym_scheme_kind : individual scheme_kind
-val build_sym_involutive_scheme : env -> inductive -> constr
+val build_sym_involutive_scheme :
+ env -> inductive -> constr * Declareops.side_effects
val sym_involutive_scheme_kind : individual scheme_kind
(** Builds a congruence scheme for an equality type *)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b991defe73..f5ab039b42 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -283,12 +283,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
begin
try
let _ = Global.lookup_constant c1' in
- mkConst c1'
+ mkConst c1', gl
with Not_found ->
let rwr_thm = Label.to_string l' in
error ("Cannot find rewrite principle "^rwr_thm^".")
end
- | _ -> pr1
+ | _ -> pr1, gl
end
| _ ->
(* cannot occur since we checked that we are in presence of
@@ -308,7 +308,10 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
| true, _, false -> rew_r2l_forward_dep_scheme_kind
in
match kind_of_term hdcncl with
- | Ind ind -> mkConst (find_scheme scheme_name ind)
+ | Ind ind ->
+ let c, eff = find_scheme scheme_name ind in
+ let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
+ mkConst c, gl
| _ -> assert false
let type_of_clause gl = function
@@ -319,7 +322,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze
let isatomic = isProd (whd_zeta hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in
- let elim = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+ let elim, gl = find_elim hdcncl lft2rgt dep cls (Some t) gl in
general_elim_clause with_evars frzevars tac cls sigma c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings)} gl
@@ -775,14 +778,16 @@ let ind_scheme_of_eq lbeq =
let kind =
if kind == InProp then Elimschemes.ind_scheme_kind_from_prop
else Elimschemes.ind_scheme_kind_from_type in
- mkConst (find_scheme kind (destInd lbeq.eq))
+ let c, eff = find_scheme kind (destInd lbeq.eq) in
+ mkConst c, eff
let discrimination_pf e (t,t1,t2) discriminator lbeq =
- let i = build_coq_I () in
- let absurd_term = build_coq_False () in
- let eq_elim = ind_scheme_of_eq lbeq in
- (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term)
+ let i = build_coq_I () in
+ let absurd_term = build_coq_False () in
+ let eq_elim, eff = ind_scheme_of_eq lbeq in
+ (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term),
+ eff
let eq_baseid = Id.of_string "e"
@@ -795,17 +800,19 @@ let apply_on_clause (f,t) clause =
| _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in
clenv_fchain argmv f_clause clause
-let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
+let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
let e = next_ident_away eq_baseid (ids_of_context env) in
let e_env = push_named (e,None,t) env in
let discriminator =
build_discriminator sigma e_env dirn (mkVar e) sort cpath in
- let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in
+ let (pf, absurd_term), eff =
+ discrimination_pf e (t,t1,t2) discriminator lbeq in
let pf_ty = mkArrow eqn absurd_term in
let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in
let pf = clenv_value_cast_meta absurd_clause in
+ let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
tclTHENS (cut_intro absurd_term)
- [onLastHypId gen_absurdity; refine pf]
+ [onLastHypId gen_absurdity; refine pf] gl
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls =
let sigma = eq_clause.evd in
@@ -1134,7 +1141,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
-let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
+let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
(* fetch the informations of the pair *)
let ceq = constr_of_global Coqlib.glob_eq in
let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in
@@ -1153,19 +1160,19 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) =
Library.require_library [Loc.ghost,eqdep_dec] (Some false);
let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing"
["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in
+ let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in
+ let gl = { gl with eff = Declareops.union_side_effects eff gl.eff } in
(* cut with the good equality and prove the requested goal *)
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[tclIDTAC; tclTHEN (apply (
- mkApp(inj2,
- [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind);
- ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
+ mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|])
)) (Auto.trivial [] [])
- ]
+ ] gl
(* not a dep eq or no decidable type found *)
end
else raise Not_dep_pair
-let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause gl =
let sigma = eq_clause.evd in
let env = eq_clause.env in
match find_positions env sigma t1 t2 with
@@ -1178,10 +1185,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
| Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 ->
errorlabstrm "Equality.inj" (str"Nothing to inject.")
| Inr posns ->
- try inject_if_homogenous_dependent_pair env sigma u
+ try inject_if_homogenous_dependent_pair env sigma u gl
with e when (Errors.noncritical e || e = Not_dep_pair) ->
inject_at_positions env sigma l2r u eq_clause posns
- (tac (clenv_value eq_clause))
+ (tac (clenv_value eq_clause)) gl
let postInjEqTac ipats c n =
match ipats with
@@ -1255,7 +1262,7 @@ let swapEquandsInConcl gls =
let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
(* find substitution scheme *)
- let eq_elim = find_elim lbeq.eq (Some false) false None None gls in
+ let eq_elim, gls = find_elim lbeq.eq (Some false) false None None gls in
(* build substitution predicate *)
let p = lambda_create (pf_env gls) (t,body) in
(* apply substitution scheme *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e14c234213..ae617a4d8a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -115,7 +115,8 @@ TACTIC EXTEND ediscriminate
END
let discrHyp id gl =
- discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl
+ discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
+ eff = gl.eff} gl
let injection_main c =
elimOnConstrWithHoles (injClause None) false c
@@ -159,7 +160,8 @@ TACTIC EXTEND einjection_as
END
let injHyp id gl =
- injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl
+ injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
+ eff = gl.eff } gl
TACTIC EXTEND dependent_rewrite
| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
@@ -765,6 +767,6 @@ END;;
mode. *)
VERNAC COMMAND EXTEND GrabEvars
[ "Grab" "Existential" "Variables" ] ->
- [ let p = Proof_global.give_me_the_proof () in
- Proof.V82.grab_evars p ]
+ [ Proof_global.with_current_proof (fun _ p ->
+ Proof.V82.grab_evars p) ]
END
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index ac4cd54423..63a5917771 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -196,7 +196,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
(str"Computed inversion goal was not closed in initial signature.");
*)
let pf = Proof.start [invEnv,invGoal] in
- Proof.run_tactic env (Proofview.V82.tactic (tclTHEN intro (onLastHypId inv_op))) pf;
+ let pf = Proof.run_tactic env
+ (Proofview.V82.tactic (tclTHEN intro (onLastHypId inv_op))) pf in
let pfterm = List.hd (Proof.partial_proof pf) in
let global_named_context = Global.named_context () in
let ownSign = ref begin
@@ -227,7 +228,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
let add_inversion_lemma name env sigma t sort dep inv_op =
let invProof = inversion_scheme env sigma t sort dep inv_op in
let entry = {
- const_entry_body = invProof;
+ const_entry_body = Future.from_val (invProof,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = None;
const_entry_opaque = false;
@@ -241,8 +242,8 @@ let add_inversion_lemma name env sigma t sort dep inv_op =
let inversion_lemma_from_goal n na (loc,id) sort dep_option inv_op =
let pts = get_pftreestate() in
- let { it=gls ; sigma=sigma } = Proof.V82.subgoals pts in
- let gl = { it = List.nth gls (n-1) ; sigma=sigma } in
+ let { it=gls ; sigma=sigma; eff=eff } = Proof.V82.subgoals pts in
+ let gl = { it = List.nth gls (n-1) ; sigma=sigma; eff=eff } in
let t =
try pf_get_hyp_typ gl id
with Not_found -> Pretype_errors.error_var_not_found_loc loc id in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index c88e67e8b0..154cad6913 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -683,7 +683,7 @@ let reset_env env =
let fold_match ?(force=false) env sigma c =
let (ci, p, c, brs) = destCase c in
let cty = Retyping.get_type_of env sigma c in
- let dep, pred, exists, sk =
+ let dep, pred, exists, (sk, eff) =
let env', ctx, body =
let ctx, pred = decompose_lam_assum p in
let env' = Environ.push_rel_context ctx env in
@@ -720,7 +720,7 @@ let fold_match ?(force=false) env sigma c =
let meths = List.map (fun br -> br) (Array.to_list brs) in
applist (mkConst sk, pars @ [pred] @ meths @ args @ [c])
in
- sk, (if exists then env else reset_env env), app
+ sk, (if exists then env else reset_env env), app, eff
let unfold_match env sigma sk app =
match kind_of_term app with
@@ -897,7 +897,7 @@ let subterm all flags (s : strategy) : strategy =
else
match try Some (fold_match env (goalevars evars) t) with Not_found -> None with
| None -> x
- | Some (cst, _, t') ->
+ | Some (cst, _, t',_) -> (* eff XXX *)
match aux env avoid t' ty cstr evars with
| Some (Some prf) ->
Some (Some { prf with
@@ -1251,7 +1251,9 @@ let assert_replacing id newt tac =
env ~init:[]
in
let (e, args) = destEvar ev in
- Goal.return (mkEvar (e, Array.of_list inst)))))
+ Goal.return
+ (mkEvar (e, Array.of_list inst))
+ Declareops.no_seff)))
in Goal.bind reft Goal.refine)
in Proofview.tclTHEN (Proofview.tclSENSITIVE sens)
(Proofview.tclFOCUS 2 2 tac)
@@ -1295,7 +1297,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
try
let res =
cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp
- in return (res, is_hyp)
+ in return (res, is_hyp) Declareops.no_seff
with
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
@@ -1316,9 +1318,9 @@ let cl_rewrite_clause_new_strat ?abs strat clause =
newfail 0 (str"setoid rewrite failed: " ++ s))
let cl_rewrite_clause_newtac' l left2right occs clause =
- Proof_global.run_tactic
+ Proof_global.with_current_proof (fun _ -> Proof.run_tactic (Global.env ())
(Proofview.tclFOCUS 1 1
- (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause))
+ (cl_rewrite_clause_new_strat (rewrite_with rewrite_unif_flags l left2right occs) clause)))
let cl_rewrite_clause_strat strat clause =
tclTHEN (tactic_init_setoid ())
@@ -1722,7 +1724,8 @@ let declare_projection n instance_id r =
let ty = Global.type_of_global r in
let c = constr_of_global r in
let term = proper_projection c ty in
- let typ = Typing.type_of (Global.env ()) Evd.empty term in
+ let env = Global.env() in
+ let typ = Typing.type_of env Evd.empty term in
let ctx, typ = decompose_prod_assum typ in
let typ =
let n =
@@ -1739,12 +1742,12 @@ let declare_projection n instance_id r =
| _ -> typ
in aux init
in
- let ctx,ccl = Reductionops.splay_prod_n (Global.env()) Evd.empty (3 * n) typ
+ let ctx,ccl = Reductionops.splay_prod_n env Evd.empty (3 * n) typ
in it_mkProd_or_LetIn ccl ctx
in
let typ = it_mkProd_or_LetIn typ ctx in
let cst =
- { const_entry_body = term;
+ { const_entry_body = Future.from_val (term,Declareops.no_seff);
const_entry_secctx = None;
const_entry_type = Some typ;
const_entry_opaque = false;
@@ -2052,26 +2055,30 @@ TACTIC EXTEND implify
[ "implify" hyp(n) ] -> [ implify n ]
END
-let rec fold_matches env sigma c =
+let rec fold_matches eff env sigma c =
map_constr_with_full_binders Environ.push_rel
(fun env c ->
match kind_of_term c with
| Case _ ->
- let cst, env, c' = fold_match ~force:true env sigma c in
- fold_matches env sigma c'
- | _ -> fold_matches env sigma c)
+ let cst, env, c',eff' = fold_match ~force:true env sigma c in
+ eff := Declareops.union_side_effects eff' !eff;
+ fold_matches eff env sigma c'
+ | _ -> fold_matches eff env sigma c)
env c
TACTIC EXTEND fold_match
[ "fold_match" constr(c) ] -> [ fun gl ->
- let _, _, c' = fold_match ~force:true (pf_env gl) (project gl) c in
- change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
+ let _, _, c', eff = fold_match ~force:true (pf_env gl) (project gl) c in
+ tclTHEN (Tactics.emit_side_effects eff)
+ (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl ]
END
TACTIC EXTEND fold_matches
-| [ "fold_matches" constr(c) ] -> [ fun gl ->
- let c' = fold_matches (pf_env gl) (project gl) c in
- change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl gl ]
+| [ "fold_matches" constr(c) ] -> [ fun gl ->
+ let eff = ref Declareops.no_seff in
+ let c' = fold_matches eff (pf_env gl) (project gl) c in
+ tclTHEN (Tactics.emit_side_effects !eff)
+ (change (Some (snd (pattern_of_constr (project gl) c))) c' onConcl) gl ]
END
TACTIC EXTEND myapply
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1b460b060b..d8e03265d5 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1046,7 +1046,7 @@ let mk_open_constr_value ist gl c =
let mk_hyp_value ist gl c = Value.of_constr (mkVar (interp_hyp ist gl c))
let mk_int_or_var_value ist c = in_gen (topwit wit_int) (interp_int_or_var ist c)
-let pack_sigma (sigma,c) = {it=c;sigma=sigma}
+let pack_sigma eff (sigma,c) = {it=c;sigma=sigma;eff=eff}
let extend_gl_hyps { it=gl ; sigma=sigma } sign =
Goal.V82.new_goal_with sigma gl sign
@@ -1317,7 +1317,7 @@ and interp_letin ist gl llc u =
(* Interprets the Match Context expressions *)
and interp_match_goal ist goal lz lr lmr =
let (gl,sigma) = Goal.V82.nf_evar (project goal) (sig_it goal) in
- let goal = { it = gl ; sigma = sigma } in
+ let goal = { it = gl ; sigma = sigma; eff = sig_eff goal } in
let hyps = pf_hyps goal in
let hyps = if lr then List.rev hyps else hyps in
let concl = pf_concl goal in
@@ -1457,11 +1457,11 @@ and interp_genarg ist gl x =
(snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
| ConstrWithBindingsArgType ->
in_gen (topwit wit_constr_with_bindings)
- (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
+ (pack_sigma (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl)
(out_gen (glbwit wit_constr_with_bindings) x)))
| BindingsArgType ->
in_gen (topwit wit_bindings)
- (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
+ (pack_sigma (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
| ListArgType ConstrArgType ->
let (sigma,v) = interp_genarg_constr_list ist gl x in
evdref := sigma;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 06ad729d44..ee92762cbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3594,6 +3594,9 @@ let abstract_subproof id tac gl =
(** ppedrot: seems legit to have abstracted subproofs as local*)
let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
let lem = mkConst cst in
+ let gl = {gl with eff =
+ Declareops.cons_side_effects
+ (Safe_typing.sideff_of_con (Global.safe_env()) cst) gl.eff} in
exact_no_check
(applist (lem,List.rev (instance_from_named_context sign)))
gl
@@ -3621,3 +3624,9 @@ let unify ?(state=full_transparent_state) x y gl =
let evd = w_unify (pf_env gl) (project gl) Reduction.CONV ~flags x y
in tclEVARS evd gl
with e when Errors.noncritical e -> tclFAIL 0 (str"Not unifiable") gl
+
+let emit_side_effects eff gl =
+ Declareops.iter_side_effects (fun e ->
+ prerr_endline ("emitting: " ^ Declareops.string_of_side_effect e))
+ eff;
+ {gl with it = [gl.it] ; eff = Declareops.union_side_effects eff gl.eff}
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index cdc8eb3757..7acd803bd8 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -398,7 +398,10 @@ val general_multi_rewrite :
val subst_one :
(bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t
+
val declare_intro_decomp_eq :
((int -> tactic) -> Coqlib.coq_eq_data * types *
(types * constr * constr) ->
clausenv -> tactic) -> unit
+
+val emit_side_effects : Declareops.side_effects -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-07 12:03:44 +0000