aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/functional_principles_proofs.ml38
-rw-r--r--plugins/funind/indfun_common.ml24
-rw-r--r--plugins/funind/recdef.ml13
-rw-r--r--plugins/ltac/evar_tactics.ml32
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/ssr/ssrcommon.ml5
-rw-r--r--proofs/refiner.mli27
-rw-r--r--tactics/tacticals.ml2
8 files changed, 97 insertions, 46 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f4200854c2..49fc513dd2 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -243,19 +243,25 @@ let change_eq env sigma hyp_id (context : rel_context) x t end_of_type =
let new_ctxt, new_end_of_type =
decompose_prod_n_assum sigma ctxt_size new_type_of_hyp
in
- let prove_new_hyp : tactic =
- tclTHEN
- (tclDO ctxt_size (Proofview.V82.of_tactic intro))
- (fun g ->
- let all_ids = pf_ids_of_hyps g in
- let new_ids, _ = list_chop ctxt_size all_ids in
- let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
- let evm, _ = pf_apply Typing.type_of g to_refine in
- tclTHEN (Refiner.tclEVARS evm) (refine to_refine) g)
+ let prove_new_hyp =
+ let open Tacticals.New in
+ let open Tacmach.New in
+ tclTHEN (tclDO ctxt_size intro)
+ (Proofview.Goal.enter (fun g ->
+ let all_ids = pf_ids_of_hyps g in
+ let new_ids, _ = list_chop ctxt_size all_ids in
+ let to_refine = applist (witness_fun, List.rev_map mkVar new_ids) in
+ let evm, _ =
+ Typing.type_of (Proofview.Goal.env g) (Proofview.Goal.sigma g)
+ to_refine
+ in
+ tclTHEN
+ (Proofview.Unsafe.tclEVARS evm)
+ (Proofview.V82.tactic (refine to_refine))))
in
let simpl_eq_tac =
change_hyp_with_using "prove_pattern_simplification" hyp_id new_type_of_hyp
- prove_new_hyp
+ (Proofview.V82.of_tactic prove_new_hyp)
in
(* observe (str "In " ++ Ppconstr.pr_id hyp_id ++ *)
(* str "removing an equation " ++ fnl ()++ *)
@@ -534,11 +540,13 @@ let instantiate_hyps_with_args (do_prove : Id.t list -> tactic) hyps args_id =
let prov_hid = pf_get_new_id hid g in
let c = mkApp (mkVar hid, args) in
let evm, _ = pf_apply Typing.type_of g c in
- tclTHENLIST
- [ Refiner.tclEVARS evm
- ; Proofview.V82.of_tactic (pose_proof (Name prov_hid) c)
- ; thin [hid]
- ; Proofview.V82.of_tactic (rename_hyp [(prov_hid, hid)]) ]
+ let open Tacticals.New in
+ Proofview.V82.of_tactic
+ (tclTHENLIST
+ [ Proofview.Unsafe.tclEVARS evm
+ ; pose_proof (Name prov_hid) c
+ ; clear [hid]
+ ; rename_hyp [(prov_hid, hid)] ])
g)
(fun (*
if not then we are in a mutual function block
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e83fe56cc9..af53f16e1f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -2,7 +2,7 @@ open Names
open Pp
open Constr
open Libnames
-open Refiner
+open Tacmach
let mk_prefix pre id = Id.of_string (pre ^ Id.to_string id)
let mk_rel_id = mk_prefix "R_"
@@ -395,7 +395,8 @@ let jmeq_refl () =
with e when CErrors.noncritical e -> raise (ToShow e)
let h_intros l =
- tclMAP (fun x -> Proofview.V82.of_tactic (Tactics.Simple.intro x)) l
+ Proofview.V82.of_tactic
+ (Tacticals.New.tclMAP (fun x -> Tactics.Simple.intro x) l)
let h_id = Id.of_string "h"
let hrec_id = Id.of_string "hrec"
@@ -427,15 +428,16 @@ let evaluable_of_global_reference r =
| _ -> assert false
let list_rewrite (rev : bool) (eqs : (EConstr.constr * bool) list) =
- tclREPEAT
- (List.fold_right
- (fun (eq, b) i ->
- tclORELSE
- (Proofview.V82.of_tactic
- ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
- i)
- (if rev then List.rev eqs else eqs)
- (tclFAIL 0 (mt ())))
+ let open Tacticals in
+ (tclREPEAT
+ (List.fold_right
+ (fun (eq, b) i ->
+ tclORELSE
+ (Proofview.V82.of_tactic
+ ((if b then Equality.rewriteLR else Equality.rewriteRL) eq))
+ i)
+ (if rev then List.rev eqs else eqs)
+ (tclFAIL 0 (mt ()))) [@ocaml.warning "-3"])
let decompose_lam_n sigma n =
if n < 0 then
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5c82ed38bb..9b2d9c4815 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -703,9 +703,16 @@ let terminate_letin (na, b, t, e) expr_info continuation_tac info g =
in
continuation_tac {info with info = new_e; forbidden_ids = new_forbidden} g
-let pf_type c tac gl =
- let evars, ty = Typing.type_of (pf_env gl) (project gl) c in
- tclTHEN (Refiner.tclEVARS evars) (tac ty) gl
+let pf_type c tac =
+ let open Tacticals.New in
+ Proofview.Goal.enter (fun gl ->
+ let env = Proofview.Goal.env gl in
+ let sigma = Proofview.Goal.sigma gl in
+ let evars, ty = Typing.type_of env sigma c in
+ tclTHEN (Proofview.Unsafe.tclEVARS evars) (tac ty))
+
+let pf_type c tac =
+ Proofview.V82.of_tactic (pf_type c (fun ty -> Proofview.V82.tactic (tac ty)))
let pf_typel l tac =
let rec aux tys l =
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 17a7121a3f..f867a47c08 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -14,10 +14,7 @@ open Constr
open Context
open CErrors
open Evar_refiner
-open Tacmach
open Tacexpr
-open Refiner
-open Evd
open Locus
open Context.Named.Declaration
open Ltac_pretype
@@ -26,7 +23,11 @@ module NamedDecl = Context.Named.Declaration
(* The instantiate tactic *)
-let instantiate_evar evk (ist,rawc) env sigma =
+let instantiate_evar evk (ist,rawc) =
+ let open Proofview.Notations in
+ Proofview.tclENV >>= fun env ->
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
let evi = Evd.find sigma evk in
let filtered = Evd.evar_filtered_env env evi in
let constrvars = Tacinterp.extract_ltac_constr_values ist filtered in
@@ -37,7 +38,8 @@ let instantiate_evar evk (ist,rawc) env sigma =
ltac_genargs = ist.Geninterp.lfun;
} in
let sigma' = w_refine (evk,evi) (lvar ,rawc) env sigma in
- tclEVARS sigma'
+ Proofview.Unsafe.tclEVARS sigma'
+ end
let evar_list sigma c =
let rec evrec acc c =
@@ -47,14 +49,15 @@ let evar_list sigma c =
evrec [] c
let instantiate_tac n c ido =
- Proofview.V82.tactic begin fun gl ->
- let env = Global.env () in
- let sigma = gl.sigma in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
+ let env = Proofview.Goal.env gl in
+ let concl = Proofview.Goal.concl gl in
let evl =
match ido with
- ConclLocation () -> evar_list sigma (pf_concl gl)
+ ConclLocation () -> evar_list sigma concl
| HypLocation (id,hloc) ->
- let decl = Environ.lookup_named id (pf_env gl) in
+ let decl = Environ.lookup_named id env in
match hloc with
InHyp ->
(match decl with
@@ -70,17 +73,16 @@ let instantiate_tac n c ido =
user_err Pp.(str "Not enough uninstantiated existential variables.");
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let evk,_ = List.nth evl (n-1) in
- instantiate_evar evk c env sigma gl
+ instantiate_evar evk c
end
let instantiate_tac_by_name id c =
- Proofview.V82.tactic begin fun gl ->
- let env = Global.env () in
- let sigma = gl.sigma in
+ Proofview.Goal.enter begin fun gl ->
+ let sigma = Proofview.Goal.sigma gl in
let evk =
try Evd.evar_key id sigma
with Not_found -> user_err Pp.(str "Unknown existential variable.") in
- instantiate_evar evk c env sigma gl
+ instantiate_evar evk c
end
let let_evar name typ =
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index d1f031b418..5ae0b2efd7 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1087,7 +1087,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacShowHyps tac ->
Proofview.V82.tactic begin
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
- end
+ end [@ocaml.warning "-3"]
| TacAbstract (t,ido) ->
let call = LtacMLCall tac in
let trace = push_trace(None,call) ist in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index e05c4c26dd..e8257b5dba 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -22,7 +22,7 @@ open Locusops
open Ltac_plugin
open Tacmach
-open Refiner
+open Tacticals
open Libnames
open Ssrmatching_plugin
open Ssrmatching
@@ -81,6 +81,9 @@ let nohint = false, []
type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma
+let project gl = gl.Evd.sigma
+let re_sig it sigma = { Evd.it = it; Evd.sigma = sigma }
+
let push_ctx a gl = re_sig (sig_it gl, a) (project gl)
let push_ctxs a gl =
re_sig (List.map (fun x -> x,a) (sig_it gl)) (project gl)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 3471f38e9e..a3cbfb5d5d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -28,42 +28,53 @@ val refiner : check:bool -> Constr.t -> unit Proofview.tactic
(** [tclIDTAC] is the identity tactic without message printing*)
val tclIDTAC : tactic
+[@@ocaml.deprecated "Use Tactical.New.tclIDTAC"]
val tclIDTAC_MESSAGE : Pp.t -> tactic
+[@@ocaml.deprecated]
(** [tclEVARS sigma] changes the current evar map *)
val tclEVARS : evar_map -> tactic
+[@@ocaml.deprecated "Use Proofview.Unsafe.tclEVARS"]
(** [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[tac2] to every resulting subgoals *)
val tclTHEN : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHEN"]
(** [tclTHENLIST [t1;..;tn]] applies [t1] THEN [t2] ... THEN [tn]. More
convenient than [tclTHEN] when [n] is large *)
val tclTHENLIST : tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENLIST"]
(** [tclMAP f [x1..xn]] builds [(f x1);(f x2);...(f xn)] *)
val tclMAP : ('a -> tactic) -> 'a list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclMAP"]
(** [tclTHEN_i tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
[(tac2 i)] to the [i]{^ th} resulting subgoal (starting from 1) *)
val tclTHEN_i : tactic -> (int -> tactic) -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHEN_i"]
(** [tclTHENLAST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
to the last resulting subgoal (previously called [tclTHENL]) *)
val tclTHENLAST : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENLAST"]
(** [tclTHENFIRST tac1 tac2 gls] applies the tactic [tac1] to [gls] and [tac2]
to the first resulting subgoal *)
val tclTHENFIRST : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENFIRST"]
(** [tclTHENS tac1 [|t1 ; ... ; tn|] gls] applies the tactic [tac1] to
[gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
an error if the number of resulting subgoals is not [n] *)
val tclTHENSV : tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSV"]
(** Same with a list of tactics *)
val tclTHENS : tactic -> tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENS"]
(** [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
@@ -71,15 +82,18 @@ val tclTHENS : tactic -> tactic list -> tactic
subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
error if the number of resulting subgoals is strictly less than [n+m] *)
val tclTHENS3PARTS : tactic -> tactic array -> tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENS3PARTS"]
(** [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSLASTn"]
(** [tclTHENSFIRSTn tac1 [t1 ; ... ; tn] tac2 gls] first applies [tac1], then
applies [t1],...,[tn] on the first [n] resulting subgoals and
[tac2] for the remaining last subgoals (previously called tclTHENST) *)
val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENSFIRSTn"]
(** A special exception for levels for the Fail tactic *)
exception FailError of int * Pp.t Lazy.t
@@ -89,15 +103,28 @@ exception FailError of int * Pp.t Lazy.t
val catch_failerror : Exninfo.iexn -> unit
val tclORELSE0 : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclORELSE0"]
val tclORELSE : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclORELSE"]
val tclREPEAT : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclREPEAT"]
val tclFIRST : tactic list -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFIRST"]
val tclTRY : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTRY"]
val tclTHENTRY : tactic -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclTHENTRY"]
val tclCOMPLETE : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclCOMPLETE"]
val tclAT_LEAST_ONCE : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclAT_LEAST_ONCE"]
val tclFAIL : int -> Pp.t -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFAIL"]
val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclFAIL_lazy"]
val tclDO : int -> tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclDO"]
val tclPROGRESS : tactic -> tactic
+[@@ocaml.deprecated "Use Tactical.New.tclPROGRESS"]
val tclSHOWHYPS : tactic -> tactic
+[@@ocaml.deprecated "Internal tactic. Do not use."]
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 07f9def2c8..374706c8f9 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -29,6 +29,8 @@ module NamedDecl = Context.Named.Declaration
type tactic = Proofview.V82.tac
+[@@@ocaml.warning "-3"]
+
let tclIDTAC = Refiner.tclIDTAC
let tclIDTAC_MESSAGE = Refiner.tclIDTAC_MESSAGE
let tclORELSE0 = Refiner.tclORELSE0
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:21:46 +0000