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

3 files changed, 8 insertions, 8 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index fa4353630..889c064b2 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1497,7 +1497,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
+      (Flags.silently (ComInductive.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
       Decl_kinds.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 357755e46..158eb9646 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -406,7 +406,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
   match fixpoint_exprl with
     | [(((_,fname),pl),_,bl,ret_type,body),_] when not is_rec ->
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
-      Command.do_definition
+      ComDefinition.do_definition
 	fname
 	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
@@ -426,7 +426,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       ComFixpoint.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
 	   (fun (evd,l) ((((_,fname),_),_,_,_,_),_) ->
@@ -616,8 +616,8 @@ and rebuild_nal aux bk bl' nal typ =
 let rebuild_bl aux bl typ = rebuild_bl aux bl typ
 
 let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) = 
-  let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
-  let ((_,_,typel),_,ctx,_) = Command.interp_fixpoint fixl ntns in
+  let fixl,ntns = ComFixpoint.extract_fixpoint_components false fixpoint_exprl in
+  let ((_,_,typel),_,ctx,_) = ComFixpoint.interp_fixpoint ~cofix:false fixl ntns in
   let constr_expr_typel = 
     with_full_print (List.map (fun c -> Constrextern.extern_constr false (Global.env ()) (Evd.from_ctx ctx) (EConstr.of_constr c))) typel in
   let fixpoint_exprl_with_new_bl = 
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 9e2774ff3..9fcb35f89 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -889,11 +889,11 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
     } in *)
   let indexpr = glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift_prm rawlist in
   (* Declare inductive *)
-  let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
-  let mie,pl,impls = Command.interp_mutual_inductive indl []
+  let indl,_,_ = ComInductive.extract_mutual_inductive_declaration_components [(indexpr,[])] in
+  let mie,pl,impls = ComInductive.interp_mutual_inductive indl []
           false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
   (* Declare the mutual inductive block with its associated schemes *)
-  ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
+  ignore (ComInductive.declare_mutual_inductive_with_eliminations mie pl impls)
 
 
 (* Find infos on identifier id. *)