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/proofview.mli | |
| parent | 4ae5a0e2dec60f753d21385b88991a9d1f0ec62d (diff) | |
| parent | 6b61b63bb8626827708024cbea1312a703a54124 (diff) | |
Merge PR #6343: [engine] Remove and deprecate `nf_enter` et al.
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 2 |
1 files changed, 2 insertions, 0 deletions
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 |