aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ssr/ssrcommon.ml28
-rw-r--r--plugins/ssr/ssrcommon.mli2
-rw-r--r--plugins/ssr/ssrequality.ml10
-rw-r--r--plugins/ssr/ssrequality.mli4
-rw-r--r--plugins/ssr/ssripats.ml6
5 files changed, 29 insertions, 21 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 7e7cd8b4a1..bcdcd0af4a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1173,7 +1173,8 @@ let genclrtac cl cs clr =
gl))
(old_cleartac clr)
-let gentac gen gl =
+let gentac gen =
+ Proofview.V82.tactic begin fun gl ->
(* ppdebug(lazy(str"sigma@gentac=" ++ pr_evar_map None (project gl))); *)
let conv, _, cl, c, clr, ucst,gl = pf_interp_gen_aux gl false gen in
ppdebug(lazy(str"c@gentac=" ++ pr_econstr_env (pf_env gl) (project gl) c));
@@ -1181,11 +1182,10 @@ let gentac gen gl =
if conv
then tclTHEN (Proofview.V82.of_tactic (convert_concl ~check:true cl)) (old_cleartac clr) gl
else genclrtac cl [c] clr gl
+ end
let genstac (gens, clr) =
- Proofview.V82.tactic ~nf_evars:false begin fun gl ->
- tclTHENLIST (old_cleartac clr :: List.rev_map gentac gens)
- gl end
+ Tacticals.New.tclTHENLIST (cleartac clr :: List.rev_map gentac gens)
let gen_tmp_ids
?(ist=Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty })) gl
@@ -1195,7 +1195,7 @@ let gen_tmp_ids
(tclTHENLIST
(List.map (fun (id,orig_ref) ->
tclTHEN
- (gentac ((None,Some(false,[])),cpattern_of_id id))
+ (Proofview.V82.of_tactic (gentac ((None,Some(false,[])),cpattern_of_id id)))
(rename_hd_prod orig_ref))
ctx.tmp_ids) gl)
;;
@@ -1222,20 +1222,24 @@ let pfLIFT f =
* since we don't want to wipe out let-ins, and it seems there is no flag
* to change that behaviour in the standard unfold code *)
let unprotecttac =
- Proofview.V82.tactic ~nf_evars:false begin fun gl ->
- let c, gl = pf_mkSsrConst "protect_term" gl in
- let prot, _ = EConstr.destConst (project gl) c in
- Tacticals.onClause (fun idopt ->
+ let open Proofview.Notations in
+ Proofview.Goal.enter begin fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let sigma, c = mkSsrConst "protect_term" env sigma in
+ let prot, _ = EConstr.destConst sigma c in
+ Proofview.Unsafe.tclEVARS sigma <*>
+ Tacticals.New.onClause (fun idopt ->
let hyploc = Option.map (fun id -> id, InHyp) idopt in
- Proofview.V82.of_tactic (Tactics.reduct_option ~check:false
+ Tactics.reduct_option ~check:false
(Reductionops.clos_norm_flags
(CClosure.RedFlags.mkflags
[CClosure.RedFlags.fBETA;
CClosure.RedFlags.fCONST prot;
CClosure.RedFlags.fMATCH;
CClosure.RedFlags.fFIX;
- CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc))
- allHypsAndConcl gl
+ CClosure.RedFlags.fCOFIX]), DEFAULTcast) hyploc)
+ allHypsAndConcl
end
let is_protect hd env sigma =
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 9229b6d384..f655457c63 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -355,7 +355,7 @@ val rewritetac : ?under:bool -> ssrdir -> EConstr.t -> tactic
type name_hint = (int * EConstr.types array) option ref
val gentac :
- Ssrast.ssrdocc * Ssrmatching.cpattern -> v82tac
+ Ssrast.ssrdocc * Ssrmatching.cpattern -> unit Proofview.tactic
val genstac :
((Ssrast.ssrhyp list option * Ssrmatching.occ) *
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 1a73bfded0..33a2eb85d9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -66,6 +66,8 @@ let simpltac = function
| SimplCut (n,m) -> tclTHEN (safe_simpltac m) (tclTRY (Proofview.V82.of_tactic (donetac n)))
| Nop -> tclIDTAC
+let simpltac s = Proofview.V82.tactic ~nf_evars:false (simpltac s)
+
(** The "congr" tactic *)
let interp_congrarg_at ist gl n rf ty m =
@@ -197,7 +199,7 @@ let simplintac occ rdx sim gl =
CErrors.user_err (Pp.str "Custom simpl tactic does not support patterns");
if occ <> None then
CErrors.user_err (Pp.str "Custom simpl tactic does not support occurrence numbers");
- simpltac (Simpl m) gl
+ Proofview.V82.of_tactic (simpltac (Simpl m)) gl
end else
let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
let simp env c _ _ = EConstr.Unsafe.to_constr (red_safe Tacred.simpl env sigma0 (EConstr.of_constr c)) in
@@ -207,7 +209,7 @@ let simplintac occ rdx sim gl =
match sim with
| Simpl m -> simptac m gl
| SimplCut (n,m) -> tclTHEN (simptac m) (tclTRY (Proofview.V82.of_tactic (donetac n))) gl
- | _ -> simpltac sim gl
+ | _ -> Proofview.V82.of_tactic (simpltac sim) gl
let rec get_evalref env sigma c = match EConstr.kind sigma c with
| Var id -> EvalVarRef id
@@ -627,7 +629,9 @@ let ssrinstancesofrule ist dir arg =
with NoMatch -> Feedback.msg_info Pp.(str"END INSTANCES"); tclIDTAC gl
end
-let ipat_rewrite occ dir c gl = rwrxtac occ None dir (project gl, c) gl
+let ipat_rewrite occ dir c = Proofview.V82.tactic ~nf_evars:false begin fun gl ->
+ rwrxtac occ None dir (project gl, c) gl
+end
let rwargtac ?under ?map_redex ist ((dir, mult), (((oclr, occ), grx), (kind, gt))) gl =
let fail = ref false in
diff --git a/plugins/ssr/ssrequality.mli b/plugins/ssr/ssrequality.mli
index fc2b75b396..1c3b1bb018 100644
--- a/plugins/ssr/ssrequality.mli
+++ b/plugins/ssr/ssrequality.mli
@@ -26,7 +26,7 @@ val mkclr : ssrclear -> ssrdocc
val nodocc : ssrdocc
val noclr : ssrdocc
-val simpltac : Ssrast.ssrsimpl -> Tacmach.tactic
+val simpltac : Ssrast.ssrsimpl -> unit Proofview.tactic
val newssrcongrtac :
int * Ssrast.ssrterm ->
@@ -61,7 +61,7 @@ val ssrrewritetac :
Ltac_plugin.Tacinterp.interp_sign ->
ssrrwarg list -> unit Proofview.tactic
-val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> Tacmach.tactic
+val ipat_rewrite : ssrocc -> ssrdir -> EConstr.t -> unit Proofview.tactic
val unlocktac :
Ltac_plugin.Tacinterp.interp_sign ->
diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 7fba7ff830..16fd5235a2 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -191,7 +191,7 @@ let isGEN_PUSH dg =
(* generalize `id` as `new_name` *)
let gen_astac id new_name =
let gen = ((None,Some(false,[])),Ssrmatching.cpattern_of_id id) in
- V82.tactic (Ssrcommon.gentac gen)
+ Ssrcommon.gentac gen
<*> Ssrcommon.tclRENAME_HD_PROD new_name
(* performs and resets all delayed generalizations *)
@@ -494,11 +494,11 @@ let rec ipat_tac1 ipat : bool tactic =
notTAC
| IOpSimpl x ->
- V82.tactic ~nf_evars:false (Ssrequality.simpltac x) <*> notTAC
+ Ssrequality.simpltac x <*> notTAC
| IOpRewrite (occ,dir) ->
Ssrcommon.tclWITHTOP
- (fun x -> V82.tactic ~nf_evars:false (Ssrequality.ipat_rewrite occ dir x)) <*> notTAC
+ (fun x -> Ssrequality.ipat_rewrite occ dir x) <*> notTAC
| IOpAbstractVars ids -> tclMK_ABSTRACT_VARS ids <*> notTAC
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:51:37 +0000