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

Patch suggested by Gaëtan Gilbert

1 files changed, 8 insertions, 13 deletions

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