From b0fcd54d69c2f404a17f7bbcd0426c0bac0080f7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 10 Mar 2018 23:41:05 +0100
Subject: [api] Move some types to their proper module.

We solve some modularity and type duplication problems by moving types
to a better place. In particular:

- We move tactics types from `Misctypes` to `Tactics` as this is their
  proper module an single user [with LTAC].

- We deprecate aliases in `Tacexpr` to such tactic types.

cc: #6512
---
 intf/misctypes.ml | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'intf')

diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 9eb6f62cc3..72db3b31cb 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -142,19 +142,6 @@ type multi =
   | RepeatStar
   | RepeatPlus
 
-type 'a core_destruction_arg =
-  | ElimOnConstr of 'a
-  | ElimOnIdent of lident
-  | ElimOnAnonHyp of int
-
-type 'a destruction_arg =
-  clear_flag * 'a core_destruction_arg
-
-type inversion_kind =
-  | SimpleInversion
-  | FullInversion
-  | FullInversionClear
-
 type ('a, 'b) gen_universe_decl = {
   univdecl_instance : 'a; (* Declared universes *)
   univdecl_extensible_instance : bool; (* Can new universes be added *)
-- 
cgit v1.2.3