[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, 16 insertions, 6 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 63768d9b8..f6e812168 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -18,7 +18,6 @@ open Tacmach
 open Constrintern
 open Prettyp
 open Printer
-open Command
 open Goptions
 open Libnames
 open Globnames
@@ -489,7 +488,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
           | Some r ->
             let sigma, env = Pfedit.get_current_context () in
             Some (snd (Hook.get f_interp_redexp env sigma r)) in
-        do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
+        ComDefinition.do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
 
 let vernac_start_proof ~atts kind l =
   let local = enforce_locality_exp atts.locality NoDischarge in
@@ -520,7 +519,7 @@ let vernac_assumption ~atts discharge kind l nl =
       List.iter (fun (lid, _) ->
 	if global then Dumpglob.dump_definition lid false "ax"
 	else Dumpglob.dump_definition lid true "var") idl) l;
-  let status = do_assumptions kind nl l in
+  let status = ComAssumption.do_assumptions kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let should_treat_as_cumulative cum poly =
@@ -592,18 +591,29 @@ let vernac_inductive ~atts cum lo finite indl =
       | _ -> user_err Pp.(str "Cannot handle mutually (co)inductive records.")
     in
     let indl = List.map unpack indl in
-    do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
+    ComInductive.do_mutual_inductive indl is_cumulative atts.polymorphic lo finite
 
 let vernac_fixpoint ~atts discharge l =
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+  (* XXX: Switch to the attribute system and match on ~atts *)
+  let do_fixpoint = if Flags.is_program_mode () then
+      ComProgramFixpoint.do_fixpoint
+    else
+      ComFixpoint.do_fixpoint
+  in
   do_fixpoint local atts.polymorphic l
 
 let vernac_cofixpoint ~atts discharge l =
   let local = enforce_locality_exp atts.locality discharge in
   if Dumpglob.dump () then
     List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
+  let do_cofixpoint = if Flags.is_program_mode () then
+      ComProgramFixpoint.do_cofixpoint
+    else
+      ComFixpoint.do_cofixpoint
+  in
   do_cofixpoint local atts.polymorphic l
 
 let vernac_scheme l =
@@ -627,14 +637,14 @@ let vernac_universe ~atts l =
     user_err ?loc:atts.loc ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
-  do_universe atts.polymorphic l
+  Declare.do_universe atts.polymorphic l
 
 let vernac_constraint ~atts l =
   if atts.polymorphic && not (Lib.sections_are_opened ()) then
     user_err ?loc:atts.loc ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
-  do_constraint atts.polymorphic l
+  Declare.do_constraint atts.polymorphic l
 
 (**********************)
 (* Modules            *)