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

9 files changed, 40 insertions, 9 deletions

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