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.
---
 vernac/classes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index efaf6c0c01..3d9c7defa6 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -411,7 +411,7 @@ let context poly l =
       in
       let nstatus = match b with
       | None ->
-        pi3 (Command.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
+        pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl
           Vernacexpr.NoInline (Loc.tag id))
       | Some b ->
         let decl = (Discharge, poly, Definition) in
-- 
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.
---
 vernac/classes.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'vernac/classes.ml')

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d9c7defa6..c2e9a5ab44 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -130,7 +130,7 @@ let declare_instance_constant k info global imps ?hook id decl poly sigma term t
     id
 
 let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
-  poly ctx (instid, bk, cl) props ?(generalize=true)
+  ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true)
   ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let ((loc, instid), pl) = instid in
@@ -215,7 +215,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
 	    Some (Inl fs)
 	| Some (_, t) -> Some (Inr t)
 	| None -> 
-	    if Flags.is_program_mode () then Some (Inl [])
+            if program_mode then Some (Inl [])
 	    else None
       in
       let subst, sigma =
@@ -297,9 +297,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
         if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
 	  declare_instance_constant k pri global imps ?hook id decl
             poly sigma (Option.get term) termtype
-	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
+        else if program_mode || refine || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
-	    if Flags.is_program_mode () then
+            if program_mode then
 	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-- 
cgit v1.2.3