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.ml40
-rw-r--r--tactics/equality.ml6
-rw-r--r--tactics/extratactics.ml46
-rw-r--r--tactics/leminv.ml4
-rw-r--r--tactics/rewrite.ml23
-rw-r--r--tactics/tacinterp.ml8
-rw-r--r--tactics/tactics.ml9
8 files changed, 53 insertions, 45 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 6ed05d6b35..373a0bb62e 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -972,7 +972,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; eff = Declareops.no_seff } in
+ let gl = { Evd.it = g; sigma = glss.Evd.sigma; } in
pr_hint_term (pf_concl gl)
(* displays the whole hint database db *)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d80b7d738a..da6e123121 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -285,8 +285,8 @@ 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;eff=eff} ->
- let res = try Some (tac {it=gl; sigma=s;eff=eff})
+ { 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
match res with
| Some gls -> sk (f gls hints) fk
@@ -294,7 +294,7 @@ let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : '
let intro_tac : atac =
lift_tactic Tactics.intro
- (fun {it = gls; sigma = s;eff=eff} info ->
+ (fun {it = gls; sigma = s;} info ->
let gls' =
List.map (fun g' ->
let env = Goal.V82.env s g' in
@@ -303,13 +303,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;eff=eff})
+ in {it = gls'; sigma = s;})
let normevars_tac : atac =
- { skft = fun sk fk {it = (gl, info); sigma = s; eff=eff} ->
+ { skft = fun sk fk {it = (gl, info); sigma = s;} ->
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';eff=eff} fk }
+ sk {it = [gl', info']; sigma = sigma';} fk }
(* Ordering of states is lexicographic on the number of remaining goals. *)
let compare (pri, _, _, res) (pri', _, _, res') =
@@ -324,9 +324,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;eff=eff} ->
+ { skft = fun sk fk {it = gl,info; sigma = s;} ->
let concl = Goal.V82.concl s gl in
- let tacgl = {it = gl; sigma = s;eff=eff} in
+ let tacgl = {it = gl; sigma = s;} in
let poss = e_possible_resolve hints info.hints concl in
let rec aux i foundone = function
| (tac, _, b, name, pp) :: tl ->
@@ -338,7 +338,7 @@ let hints_tac hints =
in
(match res with
| None -> aux i foundone tl
- | Some {it = gls; sigma = s';eff=eff} ->
+ | Some {it = gls; sigma = s';} ->
if !typeclasses_debug then
msg_debug (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp
++ str" on" ++ spc () ++ pr_ev s gl);
@@ -370,11 +370,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';eff=eff}
+ ~st:(Hint_db.transparent_state info.hints) {it = g; sigma = s';}
else info.hints;
auto_cut = derivs }
in g, info) 1 newgls in
- let glsv = {it = gls'; sigma = s';eff=eff} in
+ let glsv = {it = gls'; sigma = s';} in
sk glsv fk)
| [] ->
if not foundone && !typeclasses_debug then
@@ -417,14 +417,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; eff = Declareops.no_seff })
+ fk {it = (gl,info); sigma = s; })
| [] -> Somek2 (List.rev acc, s, fk)
- in fun {it = gls; sigma = s; eff = eff} fk ->
+ in fun {it = gls; sigma = s; } fk ->
let rec aux' = function
| Nonek2 -> fk ()
| Somek2 (res, s', fk') ->
let goals' = List.concat res in
- sk {it = goals'; sigma = s'; eff = eff } (fun () -> aux' (fk' ()))
+ sk {it = goals'; sigma = s'; } (fun () -> aux' (fk' ()))
in aux' (aux s [] (fun () -> Nonek2) gls)
let then_tac (first : atac) (second : atac) : atac =
@@ -463,8 +463,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'; eff = Declareops.no_seff } in
- (gl, { auto with auto_depth = [i]})) 1 gs; sigma = evm'; eff = Declareops.no_seff }
+ 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 get_result r =
match r with
@@ -489,11 +489,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; eff=g.eff } in
+ let gl = { it = make_autogoal ~only_classes ?st (cut_of_hints hints) None g; sigma = project g; } in
match run_tac (eauto_tac ?limit hints) gl with
| None -> raise Not_found
- | Some {it = goals; sigma = s; eff=eff} ->
- {it = List.map fst goals; sigma = s; eff=eff}
+ | Some {it = goals; sigma = s; } ->
+ {it = List.map fst goals; sigma = s;}
let real_eauto st ?limit hints p evd =
let rec aux evd fails =
@@ -539,7 +539,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; eff= Declareops.no_seff } in (* XXX eff *)
+ let gls = { it = gl ; sigma = sigma; } in
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/equality.ml b/tactics/equality.ml
index 1e01f47cd5..f5af80b0d5 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -309,7 +309,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
match kind_of_term hdcncl with
| Ind ind ->
let c, eff = find_scheme scheme_name ind in
- let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in
+ let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
mkConst c, gl
| _ -> assert false
@@ -809,7 +809,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl=
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
+ let gl = {gl with sigma = Evd.emit_side_effects eff gl.sigma } in
tclTHENS (cut_intro absurd_term)
[onLastHypId gen_absurdity; refine pf] gl
@@ -1160,7 +1160,7 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl =
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
+ let gl = { gl with sigma = Evd.emit_side_effects eff gl.sigma } in
(* cut with the good equality and prove the requested goal *)
tclTHENS (cut (mkApp (ceq,new_eq_args)))
[tclIDTAC; tclTHEN (apply (
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a935f69002..32affcbe75 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -115,8 +115,7 @@ TACTIC EXTEND ediscriminate
END
let discrHyp id gl =
- discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
- eff = gl.eff} gl
+ discr_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;} gl
let injection_main c =
elimOnConstrWithHoles (injClause None) false c
@@ -160,8 +159,7 @@ TACTIC EXTEND einjection_as
END
let injHyp id gl =
- injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl;
- eff = gl.eff } gl
+ injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl; } gl
TACTIC EXTEND dependent_rewrite
| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 63a5917771..2a2a1e3560 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -242,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; eff=eff } = Proof.V82.subgoals pts in
- let gl = { it = List.nth gls (n-1) ; sigma=sigma; eff=eff } in
+ let { it=gls ; sigma=sigma; } = Proof.V82.subgoals pts in
+ let gl = { it = List.nth gls (n-1) ; sigma=sigma; } 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.ml b/tactics/rewrite.ml
index 7d3d5da612..fafafd8534 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1189,6 +1189,15 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
| Some None -> Some None
| None -> None
+(** ppedrot: this is a workaround. The current implementation of rewrite leaks
+ evar maps. We know that we should not produce effects in here, so we reput
+ them after computing... *)
+let tclEFFECT (tac : tactic) : tactic = fun gl ->
+ let eff = Evd.eval_side_effects gl.sigma in
+ let gls = tac gl in
+ let sigma = Evd.emit_side_effects eff (Evd.drop_side_effects gls.sigma) in
+ { gls with sigma; }
+
let cl_rewrite_clause_tac ?abs strat clause gl =
let evartac evd = Refiner.tclEVARS evd in
let treat res =
@@ -1227,7 +1236,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
Refiner.tclFAIL 0
(str"Unable to satisfy the rewriting constraints."
++ fnl () ++ Himsg.explain_typeclass_error env e)
- in tac gl
+ in tclEFFECT tac gl
let bind_gl_info f =
@@ -1266,8 +1275,7 @@ let assert_replacing id newt tac =
in
let (e, args) = destEvar ev in
Goal.return
- (mkEvar (e, Array.of_list inst))
- Declareops.no_seff)))
+ (mkEvar (e, Array.of_list inst)))))
in Goal.bind reft Goal.refine)
in Proofview.tclTHEN (Proofview.tclSENSITIVE sens)
(Proofview.tclFOCUS 2 2 tac)
@@ -1311,12 +1319,13 @@ 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) Declareops.no_seff
+ in return (res, is_hyp)
with
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
++ fnl () ++ Himsg.explain_typeclass_error env e)))
- in Proofview.tclGOALBINDU info (fun i -> treat i)
+ in
+ Proofview.tclGOALBINDU info (fun i -> treat i)
let newtactic_init_setoid () =
try init_setoid (); Proofview.tclUNIT ()
@@ -1726,10 +1735,10 @@ let general_s_rewrite cl l2r occs (c,l) ~new_goals gl =
(), res
in
try
- tclWEAK_PROGRESS
+ (tclWEAK_PROGRESS
(tclTHEN
(Refiner.tclEVARS hypinfo.cl.evd)
- (cl_rewrite_clause_tac ~abs:hypinfo.abs strat cl)) gl
+ (cl_rewrite_clause_tac ~abs:hypinfo.abs strat cl))) gl
with RewriteFailure e ->
let {l2r=l2r; c1=x; c2=y} = hypinfo in
raise (Pretype_errors.PretypeError
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 63d77af662..2a00f7defd 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1045,7 +1045,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 eff (sigma,c) = {it=c;sigma=sigma;eff=eff}
+let pack_sigma (sigma,c) = {it=c;sigma=sigma;}
let extend_gl_hyps { it=gl ; sigma=sigma } sign =
Goal.V82.new_goal_with sigma gl sign
@@ -1316,7 +1316,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; eff = sig_eff goal } in
+ let goal = { it = gl ; sigma = sigma; } in
let hyps = pf_hyps goal in
let hyps = if lr then List.rev hyps else hyps in
let concl = pf_concl goal in
@@ -1456,11 +1456,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 (sig_eff gl) (interp_constr_with_bindings ist (pf_env gl) (project gl)
+ (pack_sigma (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 (sig_eff gl) (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
+ (pack_sigma (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 81ee6f19a0..298d26915f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3594,9 +3594,10 @@ 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
+ let open Declareops in
+ let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
+ let effs = cons_side_effects eff no_seff in
+ let gl = { gl with sigma = Evd.emit_side_effects effs gl.sigma; } in
exact_no_check
(applist (lem,List.rev (instance_from_named_context sign)))
gl
@@ -3629,4 +3630,4 @@ 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}
+ { it = [gl.it] ; sigma = Evd.emit_side_effects eff gl.sigma; }
generated by cgit v1.2.3 (git 2.25.1) at 2026-06-17 13:25:09 +0000