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.
---
 plugins/funind/indfun.ml |  1 +
 plugins/ltac/rewrite.ml  | 11 +++++++----
 2 files changed, 8 insertions(+), 4 deletions(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 158eb96466..071599d9c5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -407,6 +407,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
     | [(((_,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 
       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 _ _ -> ()));
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index c0060c5a7c..7faf8f6695 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1781,7 +1781,9 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
-  new_instance (Flags.is_universe_polymorphism ()) 
+  let program_mode = Flags.is_program_mode () in
+  let poly = Flags.is_universe_polymorphism () in
+  new_instance ~program_mode poly
     binders instance (Some (true, CAst.make @@ CRecord (fields)))
     ~global ~generalize:false ~refine:false Hints.empty_hint_info
 
@@ -2012,9 +2014,10 @@ let add_morphism glob binders m s n =
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-    ignore(new_instance ~global:glob poly binders instance 
-	     (Some (true, CAst.make @@ CRecord []))
-	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
+  let program_mode = Flags.is_program_mode () in
+  ignore(new_instance ~program_mode ~global:glob poly binders instance
+           (Some (true, CAst.make @@ CRecord []))
+    ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
 
-- 
cgit v1.2.3