diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/ftactic.ml | 2 | ||||
| -rw-r--r-- | engine/ftactic.mli | 2 | ||||
| -rw-r--r-- | engine/proofview.mli | 2 |
3 files changed, 5 insertions, 1 deletions
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 |