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/ltac/rewrite.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

(limited to 'plugins/ltac')

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