Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr

1 files changed, 27 insertions, 29 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bccde169f..3358951f4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1958,11 +1958,6 @@ let interp ?proof ~atts ~st c =
   (* This one is possible to handle here *)
   | VernacAbort id    -> CErrors.user_err  (str "Abort cannot be used through the Load command")
 
-  (* Handled elsewhere *)
-  | VernacProgram _
-  | VernacPolymorphic _
-  | VernacLocal _ -> assert false
-
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
       vernac_syntax_extension atts infix sl
@@ -2199,10 +2194,30 @@ let with_fail st b f =
 let interp ?(verbosely=true) ?proof ~st (loc,c) =
   let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
+  let flags f atts =
+    List.fold_left
+      (fun (polymorphism, atts) f ->
+         match f with
+         | VernacProgram when not atts.program ->
+           (polymorphism, { atts with program = true })
+         | VernacProgram ->
+           user_err Pp.(str "Program mode specified twice")
+         | VernacPolymorphic b when polymorphism = None ->
+           (Some b, atts)
+         | VernacPolymorphic _ ->
+           user_err Pp.(str "Polymorphism specified twice")
+         | VernacLocal b when Option.is_empty atts.locality ->
+           (polymorphism, { atts with locality = Some b })
+         | VernacLocal _ ->
+           user_err Pp.(str "Locality specified twice")
+      )
+      (None, atts)
+      f
+  in
   let rec control = function
-  | VernacExpr v ->
-      let atts = { loc; locality = None; polymorphic = false; } in
-      aux ~atts orig_program_mode v
+  | VernacExpr (f, v) ->
+    let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+    aux ~polymorphism ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
       current_timeout := Some n;
@@ -2212,25 +2227,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
   | VernacTime (batch, (_loc,v)) ->
       System.with_time ~batch control v;
 
-  and aux ?polymorphism ~atts isprogcmd = function
-
-    | VernacProgram c when not isprogcmd ->
-      aux ?polymorphism ~atts true c
-
-    | VernacProgram _ ->
-      user_err Pp.(str "Program mode specified twice")
-
-    | VernacPolymorphic (b, c) when polymorphism = None ->
-      aux ~polymorphism:b ~atts:atts isprogcmd 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
-
-    | VernacLocal _ ->
-      user_err Pp.(str "Locality specified twice")
+  and aux ~polymorphism ~atts : _ -> unit =
+    function
 
     | VernacLoad (_,fname) -> vernac_load control fname
 
@@ -2239,7 +2237,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
@@ -2248,7 +2246,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;