[api] Deprecate constructors of deprecated datatypes.

When deprecating some type alias [due to code refactoring] we forgot
to deprecate the constructors too. Closes #8498.

3 files changed, 27 insertions, 12 deletions

diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index dacef6e211..ecc7d3ff88 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -13,6 +13,7 @@
 open Glob_term
 open Constrexpr
 open Vernacexpr
+open Hints
 open Proof_global
 
 open Pcoq
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index e15e57a003..b4b3aead91 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -178,11 +178,11 @@ open Pputils
     | [] -> mt()
     | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z
 
-  let pr_reference_or_constr pr_c = function
+  let pr_reference_or_constr pr_c = let open Hints in function
     | HintsReference r -> pr_qualid r
     | HintsConstr c -> pr_c c
 
-  let pr_hint_mode = function
+  let pr_hint_mode = let open Hints in function
     | ModeInput -> str"+"
     | ModeNoHeadEvar -> str"!"
     | ModeOutput -> str"-"
@@ -194,6 +194,7 @@ open Pputils
   let pr_hints db h pr_c pr_pat =
     let opth = pr_opt_hintbases db  in
     let pph =
+      let open Hints in
       match h with
         | HintsResolve l ->
           keyword "Resolve " ++ prlist_with_sep sep
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 0c0204a728..13c8830b84 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -16,11 +16,11 @@ open Libnames
 type class_rawexpr = FunClass | SortClass | RefClass of qualid or_by_notation
 
 type goal_selector = Goal_select.t =
-  | SelectAlreadyFocused
-  | SelectNth of int
-  | SelectList of (int * int) list
-  | SelectId of Id.t
-  | SelectAll
+  | SelectAlreadyFocused [@ocaml.deprecated "Use Goal_select.SelectAlreadyFocused"]
+  | SelectNth of int [@ocaml.deprecated "Use Goal_select.SelectNth"]
+  | SelectList of (int * int) list [@ocaml.deprecated "Use Goal_select.SelectList"]
+  | SelectId of Id.t [@ocaml.deprecated "Use Goal_select.SelectId"]
+  | SelectAll [@ocaml.deprecated "Use Goal_select.SelectAll"]
 [@@ocaml.deprecated "Use Goal_select.t"]
 
 type goal_identifier = string
@@ -103,14 +103,14 @@ type comment =
   | CommentInt of int
 
 type reference_or_constr = Hints.reference_or_constr =
-  | HintsReference of qualid
-  | HintsConstr of constr_expr
+  | HintsReference of qualid [@ocaml.deprecated "Use Hints.HintsReference"]
+  | HintsConstr of constr_expr [@ocaml.deprecated "Use Hints.HintsConstr"]
 [@@ocaml.deprecated "Please use [Hints.reference_or_constr]"]
 
 type hint_mode = Hints.hint_mode =
-  | ModeInput (* No evars *)
-  | ModeNoHeadEvar (* No evar at the head *)
-  | ModeOutput (* Anything *)
+  | ModeInput [@ocaml.deprecated "Use Hints.ModeInput"]
+  | ModeNoHeadEvar [@ocaml.deprecated "Use Hints.ModeNoHeadEvar"]
+  | ModeOutput [@ocaml.deprecated "Use Hints.ModeOutput"]
 [@@ocaml.deprecated "Please use [Hints.hint_mode]"]
 
 type 'a hint_info_gen = 'a Typeclasses.hint_info_gen =
@@ -128,13 +128,21 @@ type 'a hints_transparency_target = 'a Hints.hints_transparency_target =
 
 type hints_expr = Hints.hints_expr =
   | HintsResolve of (Hints.hint_info_expr * bool * Hints.reference_or_constr) list
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsResolveIFF of bool * qualid list * int option
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsImmediate of Hints.reference_or_constr list
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsUnfold of qualid list
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsTransparency of qualid hints_transparency_target * bool
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsMode of qualid * Hints.hint_mode list
+                   [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsConstructors of qualid list
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
   | HintsExtern of int * constr_expr option * Genarg.raw_generic_argument
+        [@ocaml.deprecated "Use the constructor in module [Hints]"]
 [@@ocaml.deprecated "Please use [Hints.hints_expr]"]
 
 type search_restriction =
@@ -289,7 +297,9 @@ type bullet = Proof_bullet.t
 
 type 'a module_signature = 'a Declaremods.module_signature =
   | Enforce of 'a (** ... : T *)
+        [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
   | Check of 'a list (** ... <: T1 <: T2, possibly empty *)
+        [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
 [@@ocaml.deprecated "please use [Declaremods.module_signature]."]
 
 (** Which module inline annotations should we honor,
@@ -298,8 +308,11 @@ type 'a module_signature = 'a Declaremods.module_signature =
 
 type inline = Declaremods.inline =
   | NoInline
+      [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
   | DefaultInline
+      [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
   | InlineAt of int
+      [@ocaml.deprecated "Use the constructor in module [Declaremods]"]
 [@@ocaml.deprecated "please use [Declaremods.inline]."]
 
 type module_ast_inl = module_ast * Declaremods.inline