From 1923e2a87e8754e63e8d9edcdfe178a841ff96d2 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 24 Oct 2019 21:06:54 +0200
Subject: [inductive] [declare] Move full inductive declaration to declareInd

Patch suggested by Gaëtan Gilbert
---
 vernac/comInductive.mli | 21 ++++++++-------------
 1 file changed, 8 insertions(+), 13 deletions(-)

(limited to 'vernac/comInductive.mli')

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 7587bd165f..3e1e9ceaf1 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Entries
 open Vernacexpr
 open Constrexpr
 
@@ -42,22 +41,18 @@ 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"]
+
 (************************************************************************)
 (** Internal API, exported for Record                                   *)
 (************************************************************************)
 
-(** Registering a mutual inductive definition together with its
-   associated schemes *)
-
-type one_inductive_impls =
-  Impargs.manual_implicits (* for inds *) *
-  Impargs.manual_implicits list (* for constrs *)
-
-val declare_mutual_inductive_with_eliminations :
-  ?primitive_expected:bool ->
-  mutual_inductive_entry -> UnivNames.universe_binders -> one_inductive_impls list ->
-  MutInd.t
-
 val should_auto_template : Id.t -> bool -> bool
 (** [should_auto_template x b] is [true] when [b] is [true] and we
    automatically use template polymorphism. [x] is the name of the
-- 
cgit v1.2.3