[vernac] adds the “program” flag to the “atts” record

3 files changed, 11 insertions, 10 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ded0d97e6..ae62fcfeb 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2202,9 +2202,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
   let rec control = function
   | VernacExpr v ->
-      let atts = { loc; locality = None; polymorphic = false; } in
-      aux ~atts orig_program_mode v
-  | VernacFail v -> with_fail st true (fun () -> control v)
+      let atts = { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+      aux ~atts v
   | VernacTimeout (n,v) ->
       current_timeout := Some n;
       control v
@@ -2213,22 +2212,22 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
   | VernacTime (batch, (_loc,v)) ->
       System.with_time ~batch control v;
 
-  and aux ?polymorphism ~atts isprogcmd = function
+  and aux ?polymorphism ~atts = function
 
-    | VernacProgram c when not isprogcmd ->
-      aux ?polymorphism ~atts true c
+    | VernacProgram c when not atts.program ->
+      aux ?polymorphism ~atts:{ atts with program = true } c
 
     | VernacProgram _ ->
       user_err Pp.(str "Program mode specified twice")
 
     | VernacPolymorphic (b, c) when polymorphism = None ->
-      aux ~polymorphism:b ~atts:atts isprogcmd c
+      aux ~polymorphism:b ~atts:atts c
 
     | VernacPolymorphic (b, c) ->
       user_err Pp.(str "Polymorphism specified twice")
 
     | VernacLocal (b, c) when Option.is_empty atts.locality ->
-      aux ?polymorphism ~atts:{atts with locality = Some b} isprogcmd c
+      aux ?polymorphism ~atts:{atts with locality = Some b} c
 
     | VernacLocal _ ->
       user_err Pp.(str "Locality specified twice")
@@ -2240,7 +2239,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
       check_vernac_supports_polymorphism c polymorphism;
       let polymorphic = Option.default (Flags.is_universe_polymorphism ()) polymorphism in
       Flags.make_universe_polymorphism polymorphic;
-      Obligations.set_program_mode isprogcmd;
+      Obligations.set_program_mode atts.program;
       try
         vernac_timeout begin fun () ->
           let atts = { atts with polymorphic } in
@@ -2249,7 +2248,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
           else Flags.silently  (interp ?proof ~atts ~st) c;
           (* If the command is `(Un)Set Program Mode` or `(Un)Set Universe Polymorphism`,
              we should not restore the previous state of the flag... *)
-          if orig_program_mode || not !Flags.program_mode || isprogcmd then
+          if orig_program_mode || not !Flags.program_mode || atts.program then
             Flags.program_mode := orig_program_mode;
           if (Flags.is_universe_polymorphism() = polymorphic) then
             Flags.make_universe_polymorphism orig_univ_poly;
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index c0b93c163..c40ca27db 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -16,6 +16,7 @@ type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
+  program : bool;
 }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index ab3d4bfc5..c5e610f89 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -14,6 +14,7 @@ type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
+  program : bool;
 }
 
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t