[vernac] Split `command.ml` into separate files.

Over the time, `Command` grew organically and it has become now one of
the most complex files in the codebase; however, its functionality is
well separated into 4 key components that have little to do with each
other.

We thus split the file, and also document the interfaces. Some parts
of `Command` export tricky internals to use by other plugins, and it
is common that plugin writers tend to get confused, so we are more
explicit about these parts now.

This patch depends on #6413.

1 files changed, 65 insertions, 0 deletions

diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
new file mode 100644
index 000000000..82ea131e1
--- /dev/null
+++ b/vernac/comInductive.mli
@@ -0,0 +1,65 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Entries
+open Libnames
+open Vernacexpr
+open Constrexpr
+open Decl_kinds
+
+(** {6 Inductive and coinductive types} *)
+
+(** Entry points for the vernacular commands Inductive and CoInductive *)
+
+val do_mutual_inductive :
+  (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
+  polymorphic -> private_flag -> Declarations.recursivity_kind -> unit
+
+(************************************************************************)
+(** Internal API  *)
+(************************************************************************)
+
+(** Exported for Record and Funind *)
+
+(** 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 :
+  mutual_inductive_entry -> Universes.universe_binders -> one_inductive_impls list ->
+  MutInd.t
+
+(** Exported for Funind *)
+
+(** Extracting the semantical components out of the raw syntax of mutual
+   inductive declarations *)
+
+type structured_one_inductive_expr = {
+  ind_name : Id.t;
+  ind_univs : Vernacexpr.universe_decl_expr option;
+  ind_arity : constr_expr;
+  ind_lc : (Id.t * constr_expr) list
+}
+
+type structured_inductive_expr =
+  local_binder_expr list * structured_one_inductive_expr list
+
+val extract_mutual_inductive_declaration_components :
+  (one_inductive_expr * decl_notation list) list ->
+    structured_inductive_expr * (*coercions:*) qualid list * decl_notation list
+
+(** Typing mutual inductive definitions *)
+
+val interp_mutual_inductive :
+  structured_inductive_expr -> decl_notation list -> cumulative_inductive_flag ->
+  polymorphic -> private_flag -> Declarations.recursivity_kind ->
+  mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list