[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.

2 files changed, 36 insertions, 22 deletions

diff --git a/API/API.ml b/API/API.ml
index 378c03ee4..081ac2bb2 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -267,7 +267,9 @@ module Metasyntax = Metasyntax
 module Search = Search
 (* module Indschemes *)
 module Obligations = Obligations
-module Command = Command
+module ComDefinition = ComDefinition
+module ComInductive = ComInductive
+module ComFixpoint = ComFixpoint
 module Classes = Classes
 (* module Record *)
 (* module Assumptions *)
diff --git a/API/API.mli b/API/API.mli
index afde89a39..838613352 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -6050,21 +6050,51 @@ sig
   val show_term : Names.Id.t option -> Pp.t
 end
 
-module Command :
+module ComDefinition :
 sig
+  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
+    Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
+    Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit
+end
+
+module ComFixpoint :
+sig
+
   open Names
   open Constrexpr
-  open Vernacexpr
 
   type structured_fixpoint_expr = {
     fix_name : Id.t;
-    fix_univs : universe_decl_expr option;
+    fix_univs : Vernacexpr.universe_decl_expr option;
     fix_annot : Id.t Loc.located option;
     fix_binders : local_binder_expr list;
     fix_body : constr_expr option;
     fix_type : constr_expr
   }
 
+  type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list
+
+  val interp_fixpoint :
+    cofix:bool ->
+    structured_fixpoint_expr list -> Vernacexpr.decl_notation list ->
+    recursive_preentry * Univdecls.universe_decl * UState.t *
+    (EConstr.rel_context * Impargs.manual_implicits * int option) list
+
+  val extract_fixpoint_components : bool ->
+    (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
+    structured_fixpoint_expr list * Vernacexpr.decl_notation list
+
+  val do_fixpoint :
+    Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit
+
+end
+
+module ComInductive :
+sig
+  open Names
+  open Constrexpr
+  open Vernacexpr
+
   type structured_one_inductive_expr = {
     ind_name : Id.t;
     ind_univs : universe_decl_expr option;
@@ -6075,30 +6105,12 @@ sig
   type structured_inductive_expr =
     local_binder_expr list * structured_one_inductive_expr list
 
-  type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list
-
   type one_inductive_impls
 
   val do_mutual_inductive :
     (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
     Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit
 
-  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
-    Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr ->
-    Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit
-
-  val do_fixpoint :
-    Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit
-
-  val extract_fixpoint_components : bool ->
-    (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list ->
-    structured_fixpoint_expr list * Vernacexpr.decl_notation list
-
-  val interp_fixpoint :
-    structured_fixpoint_expr list -> Vernacexpr.decl_notation list ->
-    recursive_preentry * Univdecls.universe_decl * UState.t *
-      (EConstr.rel_context * Impargs.manual_implicits * int option) list
-
   val extract_mutual_inductive_declaration_components :
     (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list ->
     structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list