From 7a5688f6e2421a706c16e23e445d42f39a82e74b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 13 Dec 2017 07:18:22 +0100
Subject: [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.
---
 API/API.ml  |  4 +++-
 API/API.mli | 54 +++++++++++++++++++++++++++++++++---------------------
 2 files changed, 36 insertions(+), 22 deletions(-)

(limited to 'API')

diff --git a/API/API.ml b/API/API.ml
index 378c03ee4f..081ac2bb28 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 afde89a39b..8386133521 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
-- 
cgit v1.2.3


From 1172b52735a299dfc91aee36b30b576dfeff581c Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 13 Dec 2017 21:26:48 +0100
Subject: [flags] Make program_mode a parameter for commands in vernac.

This is useful as it allows to reflect program_mode behavior as an attribute.
---
 API/API.mli | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index 8386133521..ce33e90296 100644
--- a/API/API.mli
+++ b/API/API.mli
@@ -6052,7 +6052,9 @@ end
 
 module ComDefinition :
 sig
-  val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option ->
+  val do_definition :
+    program_mode:bool ->
+    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
@@ -6134,6 +6136,7 @@ sig
     ?abstract:bool ->
     ?global:bool ->
     ?refine:bool ->
+    program_mode:bool ->
     Decl_kinds.polymorphic ->
     Constrexpr.local_binder_expr list ->
     Vernacexpr.typeclass_constraint ->
-- 
cgit v1.2.3