[inductive] [declare] Move full inductive declaration to declareInd

Patch suggested by Gaëtan Gilbert

1 files changed, 13 insertions, 4 deletions

diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index 6db09ad2bd..df8895a999 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -8,7 +8,16 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** [declare_mind me] declares a block of inductive types with
-   their constructors in the current section; it returns the path of
-   the whole block and a boolean indicating if it is a primitive record. *)
-val declare_mind : Entries.mutual_inductive_entry -> Libobject.object_name * bool
+(** 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
+  -> Entries.mutual_inductive_entry
+  -> UnivNames.universe_binders
+  -> one_inductive_impls list
+  -> Names.MutInd.t