From d83e95cce852c5471593a27d0fdca39a262c885f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 20 May 2020 00:47:21 +0200
Subject: [declare] [api] Removal of deprecated functions

The previous refactoring in `Declare` to add `CInfo.t` makes this a
good moment to clean overlays up w.r.t. deprecation.

All cases but one is just a matter of simple renaming, for the other
the use of an internal API is replaced by newer API.
---
 vernac/comInductive.mli | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'vernac/comInductive.mli')

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 984581152a..9c876787a3 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -41,14 +41,6 @@ val do_mutual_inductive
 
 val make_cases : Names.inductive -> string list list
 
-val declare_mutual_inductive_with_eliminations
-  : ?primitive_expected:bool
-  -> Entries.mutual_inductive_entry
-  -> UnivNames.universe_binders
-  -> DeclareInd.one_inductive_impls list
-  -> Names.MutInd.t
-  [@@ocaml.deprecated "Please use DeclareInd.declare_mutual_inductive_with_eliminations"]
-
 val interp_mutual_inductive_constr
   : sigma:Evd.evar_map
   -> template:bool option
-- 
cgit v1.2.3