aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/doc/changes.md2
-rw-r--r--engine/ftactic.ml2
-rw-r--r--engine/ftactic.mli2
-rw-r--r--engine/proofview.mli2
-rw-r--r--plugins/btauto/refl_btauto.ml4
-rw-r--r--plugins/firstorder/rules.ml2
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/extratactics.ml44
-rw-r--r--plugins/ltac/tacinterp.ml10
-rw-r--r--plugins/ltac/tactic_debug.ml2
-rw-r--r--plugins/micromega/coq_micromega.ml8
-rw-r--r--plugins/omega/coq_omega.ml12
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--plugins/ssr/ssrparser.ml42
-rw-r--r--stm/stm.ml4
-rw-r--r--tactics/autorewrite.ml2
-rw-r--r--tactics/class_tactics.ml2
-rw-r--r--tactics/equality.ml2
-rw-r--r--tactics/tactics.ml2
20 files changed, 37 insertions, 33 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 1eea2443fe..4f3d793ed4 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -219,7 +219,7 @@ General deprecation
Proof engine
- Due to the introduction of `EConstr` in 8.7, it is not necessary to
+- Due to the introduction of `EConstr` in 8.7, it is not necessary to
track "goal evar normal form status" anymore, thus the type `'a
Proofview.Goal.t` loses its ghost argument. This may introduce some
minor incompatibilities at the typing level. Code-wise, things
diff --git a/engine/ftactic.ml b/engine/ftactic.ml
index e23a03c0c7..b371884ba4 100644
--- a/engine/ftactic.ml
+++ b/engine/ftactic.ml
@@ -61,7 +61,7 @@ let nf_enter f =
(fun gl ->
gl >>= fun gl ->
Proofview.Goal.normalize gl >>= fun nfgl ->
- Proofview.V82.wrap_exceptions (fun () -> f nfgl))
+ Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"]
let enter f =
bind goals
diff --git a/engine/ftactic.mli b/engine/ftactic.mli
index 6c389b2d67..3c4fa6f4e8 100644
--- a/engine/ftactic.mli
+++ b/engine/ftactic.mli
@@ -42,6 +42,8 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** {5 Focussing} *)
val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t
+[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
+
(** Enter a goal. The resulting tactic is focussed. *)
val enter : (Proofview.Goal.t -> 'a t) -> 'a t
diff --git a/engine/proofview.mli b/engine/proofview.mli
index a9666e4f90..0bb3229a9b 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -497,6 +497,7 @@ module Goal : sig
(** Normalises the argument goal. *)
val normalize : t -> t tactic
+ [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"]
(** [concl], [hyps], [env] and [sigma] given a goal [gl] return
respectively the conclusion of [gl], the hypotheses of [gl], the
@@ -514,6 +515,7 @@ module Goal : sig
the current goal is also given as an argument to [t]. The goal
is normalised with respect to evars. *)
val nf_enter : (t -> unit tactic) -> unit tactic
+ [@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"]
(** Like {!nf_enter}, but does not normalize the goal beforehand. *)
val enter : (t -> unit tactic) -> unit tactic
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index c2bc8c079c..b0f97c59b8 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -224,7 +224,7 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let eq = Lazy.force eq in
let concl = EConstr.Unsafe.to_constr concl in
@@ -240,7 +240,7 @@ module Btauto = struct
end
let tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let concl = EConstr.Unsafe.to_constr concl in
let sigma = Tacmach.New.project gl in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b13580bc03..3ae777cc9a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -34,7 +34,7 @@ type lseqtac= GlobRef.t -> seqtac
type 'a with_backtracking = tactic -> 'a
let wrap n b continue seq =
- Proofview.Goal.nf_enter begin fun gls ->
+ Proofview.Goal.enter begin fun gls ->
Control.check_for_interrupt ();
let nc = Proofview.Goal.hyps gls in
let env=pf_env gls in
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 73490a2dfd..b0277e9cc2 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -99,7 +99,7 @@ let let_evar name typ =
let hget_evar n =
let open EConstr in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let evl = evar_list sigma concl in
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index d42876e23e..ba3fa6fa0d 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -781,9 +781,9 @@ END
(**********************************************************************)
TACTIC EXTEND transparent_abstract
-| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) ] -> [ Proofview.Goal.enter begin fun gl ->
Tactics.tclABSTRACT ~opaque:false None (Tacinterp.tactic_of_value ist t) end ]
-| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.nf_enter begin fun gl ->
+| [ "transparent_abstract" tactic3(t) "using" ident(id) ] -> [ Proofview.Goal.enter begin fun gl ->
Tactics.tclABSTRACT ~opaque:false (Some id) (Tacinterp.tactic_of_value ist t) end ]
END
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 414173ca79..67ffae59cc 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1469,7 +1469,7 @@ and interp_genarg ist x : Val.t Ftactic.t =
independently of goals. *)
and interp_genarg_constr_list ist x =
- Ftactic.nf_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let lc = Genarg.out_gen (glbwit (wit_list wit_constr)) x in
@@ -1601,7 +1601,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacMutualFix (id,n,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual fix>") begin
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,n,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1616,7 +1616,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacMutualCofix (id,l) ->
(* spiwack: until the tactic is in the monad *)
Proofview.Trace.name_tactic (fun () -> Pp.str"<mutual cofix>") begin
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let f sigma (id,c) =
let (sigma,c_interp) = interp_type ist env sigma c in
@@ -1696,7 +1696,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInductionDestruct (isrec,ev,(l,el)) ->
(* spiwack: some unknown part of destruct needs the goal to be
prenormalised. *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = project gl in
let sigma,l =
@@ -1723,7 +1723,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Conversion *)
| TacReduce (r,cl) ->
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
(Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl))
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 105b5c59ae..48d677a864 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -58,7 +58,7 @@ let db_pr_goal gl =
str" " ++ pc) ++ fnl ()
let db_pr_goal =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let pg = db_pr_goal gl in
Proofview.tclLIFT (msg_tac_notice (str "Goal:" ++ fnl () ++ pg))
end
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index f22147f8b0..e0a369ca5f 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1456,7 +1456,7 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*
let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
let vm = dump_varmap (spec.typ) (vm_of_list env) in
(* todo : directly generate the proof term - or generalize before conversion? *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclTHENLIST
[
Tactics.change_concl
@@ -1709,7 +1709,7 @@ let micromega_gen
(normalise:'cst atom -> 'cst mc_cnf)
unsat deduce
spec dumpexpr prover tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Tacmach.New.pf_concl gl in
let hyps = Tacmach.New.pf_hyps_types gl in
@@ -1787,7 +1787,7 @@ let micromega_order_changer cert env ff =
let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
let vm = dump_varmap (typ) (vm_of_list env) in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclTHENLIST
[
(Tactics.change_concl
@@ -1817,7 +1817,7 @@ let micromega_genr prover tac =
proof_typ = Lazy.force coq_QWitness ;
dump_proof = dump_psatz coq_Q dump_q
} in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Tacmach.New.project gl in
let concl = Tacmach.New.pf_concl gl in
let hyps = Tacmach.New.pf_hyps_types gl in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e14c4e2ec1..abae6940fa 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -588,7 +588,7 @@ let abstract_path sigma typ path t =
let focused_simpl path =
let open Tacmach.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in
convert_concl_no_check newc DEFAULTcast
end
@@ -656,7 +656,7 @@ let new_hole env sigma c =
let clever_rewrite_base_poly typ p result theorem =
let open Tacmach.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let full = pf_concl gl in
let env = pf_env gl in
let (abstracted,occ) = abstract_path (project gl) typ (List.rev p) full in
@@ -708,7 +708,7 @@ let refine_app gl t =
let clever_rewrite p vpath t =
let open Tacmach.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let full = pf_concl gl in
let (abstracted,occ) = abstract_path (project gl) (Lazy.force coq_Z) (List.rev p) full in
let vargs = List.map (fun p -> occurrence (project gl) p occ) vpath in
@@ -1763,7 +1763,7 @@ let onClearedName id tac =
(* so renaming may be necessary *)
tclTHEN
(tclTRY (clear [id]))
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let id = fresh_id Id.Set.empty id gl in
tclTHEN (introduction id) (tac id)
end)
@@ -1771,7 +1771,7 @@ let onClearedName id tac =
let onClearedName2 id tac =
tclTHEN
(tclTRY (clear [id]))
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let id1 = fresh_id Id.Set.empty (add_suffix id "_left") gl in
let id2 = fresh_id Id.Set.empty (add_suffix id "_right") gl in
tclTHENLIST [ introduction id1; introduction id2; tac id1 id2 ]
@@ -1956,7 +1956,7 @@ let destructure_goal =
try
let dec = decidability t in
tclTHEN
- (Proofview.Goal.nf_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
refine_app gl (mkApp (Lazy.force coq_dec_not_not, [| t; dec |]))
end)
intro
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index e603480656..930048400a 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1049,7 +1049,7 @@ let resolution unsafe sigma env (reified_concl,reified_hyps) systems_list =
Tactics.apply (Lazy.force coq_I)
let total_reflexive_omega_tactic unsafe =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Coqlib.check_required_library ["Coq";"romega";"ROmega"];
rst_omega_eq ();
rst_omega_var ();
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1f3c758e5c..f2f236f448 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1088,7 +1088,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;;
(** Basic tactics *)
-let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl ->
+let rec fst_prod red tac = Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
match EConstr.kind (Proofview.Goal.sigma gl) concl with
| Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 8b9c94f2db..a7aae5bd31 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1949,7 +1949,7 @@ ARGUMENT EXTEND ssrexactarg TYPED AS ssrapplyarg PRINTED BY pr_ssraarg
END
let vmexacttac pf =
- Goal.nf_enter begin fun gl ->
+ Goal.enter begin fun gl ->
exact_no_check (EConstr.mkCast (pf, _vmcast, Tacmach.New.pf_concl gl))
end
diff --git a/stm/stm.ml b/stm/stm.ml
index 635bf9bf31..b7ba163309 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2009,7 +2009,7 @@ end = struct (* {{{ *)
1 goals in
TaskQueue.join queue;
let assign_tac : unit Proofview.tactic =
- Proofview.(Goal.nf_enter begin fun g ->
+ Proofview.(Goal.enter begin fun g ->
let gid = Goal.goal g in
let f =
try List.assoc gid res
@@ -2301,7 +2301,7 @@ let known_state ~doc ?(redefine_qed=false) ~cache id =
| `Leaks -> Exninfo.iraise exn
| `ValidBlock { base_state; goals_to_admit; recovery_command } -> begin
let tac =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
if CList.mem_f Evar.equal
(Proofview.Goal.goal gl) goals_to_admit then
Proofview.give_up else Proofview.tclUNIT ()
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index c8fd0b7a75..8e296de617 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -162,7 +162,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
| None ->
(* try to rewrite in all hypothesis
(except maybe the rewritten one) *)
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let ids = Tacmach.New.pf_ids_of_hyps gl in
try_do_hyps (fun id -> id) ids
end)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9c5fdcd1ce..3456d13bbe 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -416,7 +416,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
if get_typeclasses_filtered_unification () then
let tac =
matches_pattern concl p <*>
- Proofview.Goal.nf_enter
+ Proofview.Goal.enter
(fun gl -> unify_resolve_refine poly flags gl (c,None,clenv)) in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0e39215701..d0f4b2c680 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -249,7 +249,7 @@ let rewrite_elim with_evars frzevars cls c e =
let tclNOTSAMEGOAL tac =
let goal gl = Proofview.Goal.goal gl in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = project gl in
let ev = goal gl in
tac >>= fun () ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 95d545b046..6999b17d8e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2824,7 +2824,7 @@ let generalize_goal gl i ((occs,c,b),na as o) (cl,sigma) =
let generalize_dep ?(with_let=false) c =
let open Tacmach.New in
let open Tacticals.New in
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = pf_env gl in
let sign = Proofview.Goal.hyps gl in
let sigma = project gl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:30:48 +0000