diff options
| author | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-09-25 10:43:57 +0200 |
| commit | 7eb8a7eb8d23ffaf149f71a46fb1b089b90db7f8 (patch) | |
| tree | aa480ca16c64e5c1e04ac31dd9bc8066f44840c1 /engine/ftactic.mli | |
| parent | 4ae5a0e2dec60f753d21385b88991a9d1f0ec62d (diff) | |
| parent | 6b61b63bb8626827708024cbea1312a703a54124 (diff) | |
Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al.
Diffstat (limited to 'engine/ftactic.mli')
| -rw-r--r-- | engine/ftactic.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |