From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
---
 kernel/indtypes.mli | 19 -------------------
 1 file changed, 19 deletions(-)

(limited to 'kernel/indtypes.mli')

diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7810c1723e..1b8e4208ff 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -9,28 +9,9 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Declarations
 open Environ
 open Entries
 
 (** Check an inductive. *)
 val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** Deprecated *)
-type inductive_error =
-  | NonPos of env * constr * constr
-  | NotEnoughArgs of env * constr * constr
-  | NotConstructor of env * Id.t * constr * constr * int * int
-  | NonPar of env * constr * int * constr * constr
-  | SameNamesTypes of Id.t
-  | SameNamesConstructors of Id.t
-  | SameNamesOverlap of Id.t list
-  | NotAnArity of env * constr
-  | BadEntry
-  | LargeNonPropInductiveNotInType
-  | BadUnivs
-[@@ocaml.deprecated "Use [Type_errors.inductive_error]"]
-
-exception InductiveError of Type_errors.inductive_error
-[@@ocaml.deprecated "Use [Type_errors.InductiveError]"]
-- 
cgit v1.2.3