[flags] Make program_mode a parameter for commands in vernac.

This is useful as it allows to reflect program_mode behavior as an attribute.

6 files changed, 13 insertions, 10 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index 3d9c7defa..c2e9a5ab4 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];
diff --git a/vernac/classes.mli b/vernac/classes.mli
index c0f03227c..d47c6a6f8 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -41,6 +41,7 @@ val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
   ?global:bool -> (** Not global by default. *)
   ?refine:bool -> (** Allow refinement *)
+  program_mode:bool ->
   Decl_kinds.polymorphic ->
   local_binder_expr list ->
   Vernacexpr.typeclass_constraint ->
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index c8b289c9d..883121479 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -104,11 +104,11 @@ let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd Evd.empty;
   ce
 
-let do_definition ident k univdecl bl red_option c ctypopt hook =
+let do_definition ~program_mode ident k univdecl bl red_option c ctypopt hook =
   let (ce, evd, univdecl, imps as def) =
     interp_definition univdecl bl (pi2 k) red_option c ctypopt
   in
-    if Flags.is_program_mode () then
+    if program_mode then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
       assert(Safe_typing.empty_private_constants = sideff);
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 8dcd31f25..4a65c1e91 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -14,7 +14,8 @@ open Constrexpr
 
 (** {6 Definitions/Let} *)
 
-val do_definition : Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
+val do_definition : program_mode:bool ->
+  Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option ->
   local_binder_expr list -> red_expr option -> constr_expr ->
   constr_expr option -> unit Lemmas.declaration_hook -> unit
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 181068089..58e4b00fc 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1185,7 +1185,6 @@ let init_program () =
   Coqlib.check_required_library ["Coq";"Init";"Specif"];
   Coqlib.check_required_library ["Coq";"Program";"Tactics"]
 
-
 let set_program_mode c =
   if c then
     if !Flags.program_mode then ()
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f6e812168..f5aa15e75 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -478,6 +478,7 @@ let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def =
   | Discharge -> Dumpglob.dump_definition lid true "var"
   | Local | Global -> Dumpglob.dump_definition lid false "def"
   in
+  let program_mode = Flags.is_program_mode () in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
           start_proof_and_print (local, atts.polymorphic, DefinitionBody kind)
@@ -488,7 +489,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
-        ComDefinition.do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook)
+        ComDefinition.do_definition ~program_mode 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
@@ -841,7 +842,8 @@ let vernac_identity_coercion ~atts id qids qidt =
 let vernac_instance ~atts abst sup inst props pri =
   let global = not (make_section_locality atts.locality) in
   Dumpglob.dump_constraint inst false "inst";
-  ignore(Classes.new_instance ~abstract:abst ~global atts.polymorphic sup inst props pri)
+  let program_mode = Flags.is_program_mode () in
+  ignore(Classes.new_instance ~program_mode ~abstract:abst ~global atts.polymorphic sup inst props pri)
 
 let vernac_context ~atts l =
   if not (Classes.context atts.polymorphic l) then Feedback.feedback Feedback.AddedAxiom