Merge PR #6419: [vernac] Split `command.ml` into separate files.

3 files changed, 9 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..071599d9c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -406,7 +406,8 @@ 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
+        ~program_mode:false
 	fname
 	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
@@ -426,7 +427,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 +617,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. *)