Merge PR #8499: [api] Deprecate constructors of deprecated datatypes.

13 files changed, 68 insertions, 22 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 489a40ed09..e114a0119e 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -98,7 +98,7 @@ let functional_induction with_clean c princl pat =
       List.map2
         (fun c pat ->
           ((None,
-            Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
+            Tactics.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))),
            (None,pat),
            None))
         (args@c_list)
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 8dad6260ae..d42876e23e 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -26,6 +26,7 @@ open Termops
 open Equality
 open Namegen
 open Tactypes
+open Tactics
 open Proofview.Notations
 open Vernacinterp
 
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index c13bd69daf..929390b1c4 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -314,22 +314,23 @@ GEXTEND Gram
   range_selector_or_nth:
     [ [ n = natural ; "-" ; m = natural;
         l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
-          SelectList ((n, m) :: Option.default [] l)
+          Goal_select.SelectList ((n, m) :: Option.default [] l)
       | n = natural;
         l = OPT [","; l = LIST1 range_selector SEP "," -> l] ->
+          let open Goal_select in
           Option.cata (fun l -> SelectList ((n, n) :: l)) (SelectNth n) l ] ]
   ;
   selector_body:
   [ [ l = range_selector_or_nth -> l
-    | test_bracket_ident; "["; id = ident; "]" -> SelectId id ] ]
+    | test_bracket_ident; "["; id = ident; "]" -> Goal_select.SelectId id ] ]
   ;
   selector:
     [ [ IDENT "only"; sel = selector_body; ":" -> sel ] ]
   ;
   toplevel_selector:
     [ [ sel = selector_body; ":" -> sel
-    |   "!"; ":" -> SelectAlreadyFocused
-    |   IDENT "all"; ":" -> SelectAll ] ]
+    |   "!"; ":" -> Goal_select.SelectAlreadyFocused
+    |   IDENT "all"; ":" -> Goal_select.SelectAll ] ]
   ;
   tactic_mode:
     [ [ g = OPT toplevel_selector; tac = G_vernac.query_command -> tac g
@@ -346,7 +347,7 @@ GEXTEND Gram
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
         tac = Pltac.tactic ->
-          Vernacexpr.HintsExtern (n,c, in_tac tac) ] ]
+          Hints.HintsExtern (n,c, in_tac tac) ] ]
   ;
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
@@ -373,6 +374,7 @@ let _ = declare_int_option {
 }
 
 let vernac_solve n info tcom b =
+  let open Goal_select in
   let status = Proof_global.with_current_proof (fun etac p ->
     let with_end_tac = if b then Some etac else None in
     let global = match n with SelectAll | SelectList _ -> true | _ -> false in
@@ -432,7 +434,7 @@ VERNAC tactic_mode EXTEND VernacSolve
       VtLater
     ] -> [
       let t = rm_abstract t in
-      vernac_solve SelectAll n t def
+      vernac_solve Goal_select.SelectAll n t def
     ]
 END
 
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 2e1ce814aa..571595be70 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -21,6 +21,8 @@ open Constrexpr
 open Libnames
 open Tok
 open Tactypes
+open Tactics
+open Inv
 open Locus
 open Decl_kinds
 
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 4357689ee2..803d35d07c 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -28,6 +28,7 @@ open Printer
 
 open Tacexpr
 open Tacarg
+open Tactics
 
 module Tag =
 struct
@@ -507,7 +508,7 @@ let string_of_genarg_arg (ArgumentType arg) =
   let pr_destruction_arg prc prlc (clear_flag,h) =
     pr_clear_flag clear_flag (pr_core_destruction_arg prc prlc) h
 
-  let pr_inversion_kind = function
+  let pr_inversion_kind = let open Inv in function
     | SimpleInversion -> primitive "simple inversion"
     | FullInversion -> primitive "inversion"
     | FullInversionClear -> primitive "inversion_clear"
@@ -516,7 +517,7 @@ let string_of_genarg_arg (ArgumentType arg) =
     if Int.equal i j then int i
     else int i ++ str "-" ++ int j
 
-let pr_goal_selector toplevel = function
+let pr_goal_selector toplevel = let open Goal_select in function
   | SelectAlreadyFocused -> str "!:"
   | SelectNth i -> int i ++ str ":"
   | SelectList l -> prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str ":"
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 59b748e25e..11d13d3a2f 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -37,16 +37,24 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
 
 type goal_selector = Goal_select.t =
   | SelectAlreadyFocused
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectNth of int
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectList of (int * int) list
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectId of Id.t
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectAll
-[@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
+[@@ocaml.deprecated "Use [Goal_select.t]"]
 
 type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
   | ElimOnConstr of 'a
+    [@ocaml.deprecated "Use constructors in [Tactics]"]
   | ElimOnIdent of lident
+    [@ocaml.deprecated "Use constructors in [Tactics]"]
   | ElimOnAnonHyp of int
+    [@ocaml.deprecated "Use constructors in [Tactics]"]
 [@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
 
 type 'a destruction_arg =
@@ -55,8 +63,11 @@ type 'a destruction_arg =
 
 type inversion_kind = Inv.inversion_kind =
   | SimpleInversion
+    [@ocaml.deprecated "Use constructors in [Inv]"]
   | FullInversion
+    [@ocaml.deprecated "Use constructors in [Inv]"]
   | FullInversionClear
+    [@ocaml.deprecated "Use constructors in [Inv]"]
 [@@ocaml.deprecated "Use Tactics.inversion_kind"]
 
 type ('c,'d,'id) inversion_strength =
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 3a0badb28f..6b131edaac 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -37,16 +37,24 @@ type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use
 
 type goal_selector = Goal_select.t =
   | SelectAlreadyFocused
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectNth of int
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectList of (int * int) list
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectId of Id.t
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
   | SelectAll
+    [@ocaml.deprecated "Use constructors in [Goal_select]"]
 [@@ocaml.deprecated "Use Vernacexpr.goal_selector"]
 
 type 'a core_destruction_arg = 'a Tactics.core_destruction_arg =
   | ElimOnConstr of 'a
+    [@ocaml.deprecated "Use constructors in [Tactics]"]
   | ElimOnIdent of lident
+    [@ocaml.deprecated "Use constructors in [Tactics]"]
   | ElimOnAnonHyp of int
+    [@ocaml.deprecated "Use constructors in [Tactics]"]
 [@@ocaml.deprecated "Use Tactics.core_destruction_arg"]
 
 type 'a destruction_arg =
@@ -55,8 +63,11 @@ type 'a destruction_arg =
 
 type inversion_kind = Inv.inversion_kind =
   | SimpleInversion
+    [@ocaml.deprecated "Use constructors in [Inv]"]
   | FullInversion
+    [@ocaml.deprecated "Use constructors in [Inv]"]
   | FullInversionClear
+    [@ocaml.deprecated "Use constructors in [Inv]"]
 [@@ocaml.deprecated "Use Tactics.inversion_kind"]
 
 type ('c,'d,'id) inversion_strength =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 1444800624..5501cf92a5 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -29,6 +29,7 @@ open Stdarg
 open Tacarg
 open Namegen
 open Tactypes
+open Tactics
 open Locus
 
 (** Globalization of tactic expressions :
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 71da6c7667..414173ca79 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -37,6 +37,7 @@ open Tacarg
 open Printer
 open Pretyping
 open Tactypes
+open Tactics
 open Locus
 open Tacintern
 open Taccoerce
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index dd799dc131..4626378db6 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -15,6 +15,7 @@ open Genarg
 open Stdarg
 open Tacarg
 open Tactypes
+open Tactics
 open Globnames
 open Genredexpr
 open Patternops
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