From 53870b7f6890a593d1da93706f3d020a79d226e5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 18 Sep 2018 15:22:12 +0200
Subject: [api] Remove (most) 8.9 deprecated objects.

A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
---
 plugins/ltac/tacexpr.ml  | 35 -----------------------------------
 plugins/ltac/tacexpr.mli | 35 -----------------------------------
 2 files changed, 70 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml
index 11d13d3a2f..8731cbf60d 100644
--- a/plugins/ltac/tacexpr.ml
+++ b/plugins/ltac/tacexpr.ml
@@ -35,41 +35,6 @@ type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
-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 [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 =
-  clear_flag * 'a Tactics.core_destruction_arg
-[@@ocaml.deprecated "Use Tactics.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 =
   | NonDepInversion of
       Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli
index 6b131edaac..9958d6dcda 100644
--- a/plugins/ltac/tacexpr.mli
+++ b/plugins/ltac/tacexpr.mli
@@ -35,41 +35,6 @@ type advanced_flag = bool  (* true = advanced         false = basic *)
 type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *)
 
-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 =
-  clear_flag * 'a Tactics.core_destruction_arg
-[@@ocaml.deprecated "Use Tactics.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 =
   | NonDepInversion of
       Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option
-- 
cgit v1.2.3