diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-29 14:25:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-01 23:28:38 +0200 |
| commit | f8190123ff989e38f9e196260119453b13739ded (patch) | |
| tree | 078e8778e2bc6da1b5b7ca2e641a931e8d08ddfe /vernac | |
| parent | 033c32a32fedcf2160bb38a3fed55efa9d1c2b77 (diff) | |
[api] Fix wrong deprecation warning (#7915)
Fixes: #7915.
Due to a change in the original misctypes removal PR, the deprecation
notice went out of sync.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/misctypes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/vernac/misctypes.ml b/vernac/misctypes.ml index ae725efaa..ef9cd3c35 100644 --- a/vernac/misctypes.ml +++ b/vernac/misctypes.ml @@ -17,10 +17,10 @@ type 'a or_by_notation = 'a Constrexpr.or_by_notation [@@ocaml.deprecated "use [Constrexpr.or_by_notation]"] type intro_pattern_naming_expr = Namegen.intro_pattern_naming_expr = - | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] - | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Evarutil]"] - | IntroAnonymous [@ocaml.deprecated "Use version in [Evarutil]"] -[@@ocaml.deprecated "use [Evarutil.intro_pattern_naming_expr]"] + | IntroIdentifier of Id.t [@ocaml.deprecated "Use version in [Namegen]"] + | IntroFresh of Id.t [@ocaml.deprecated "Use version in [Namegen]"] + | IntroAnonymous [@ocaml.deprecated "Use version in [Namegen]"] +[@@ocaml.deprecated "use [Namegen.intro_pattern_naming_expr]"] type 'a or_var = 'a Locus.or_var = | ArgArg of 'a [@ocaml.deprecated "Use version in [Locus]"] |