From f8190123ff989e38f9e196260119453b13739ded Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 29 Jun 2018 14:25:37 +0200 Subject: [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. --- vernac/misctypes.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac') 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]"] -- cgit v1.2.3