[vernac] vernac_expr no longer recursive

2 files changed, 30 insertions, 31 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ae62fcfeb..814dc1411 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1959,11 +1959,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
@@ -2200,10 +2195,31 @@ 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; program = orig_program_mode; } in
-      aux ~atts 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;
       control v
@@ -2212,25 +2228,8 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
   | VernacTime (batch, (_loc,v)) ->
       System.with_time ~batch control v;
 
-  and aux ?polymorphism ~atts = function
-
-    | 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 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} c
-
-    | VernacLocal _ ->
-      user_err Pp.(str "Locality specified twice")
+  and aux ~polymorphism ~atts : _ -> unit =
+    function
 
     | VernacLoad (_,fname) -> vernac_load control fname
 
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 4fdc78dd2..3932d1c7b 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -12,14 +12,14 @@
 open Vernacexpr
 
 let rec under_control = function
-  | VernacExpr c -> c
+  | VernacExpr (_, c) -> c
   | VernacRedirect (_,(_,c))
   | VernacTime (_,(_,c))
   | VernacFail c
   | VernacTimeout (_,c) -> under_control c
 
 let rec has_Fail = function
-  | VernacExpr c -> false
+  | VernacExpr _ -> false
   | VernacRedirect (_,(_,c))
   | VernacTime (_,(_,c))
   | VernacTimeout (_,c) -> has_Fail c
@@ -45,8 +45,8 @@ let rec is_deep_navigation_vernac = function
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
 let is_reset = function
-  | VernacExpr VernacResetInitial
-  | VernacExpr (VernacResetName _) -> true
+  | VernacExpr ( _, VernacResetInitial)
+  | VernacExpr (_, VernacResetName _) -> true
   | _ -> false
 
 let is_debug cmd = match under_control cmd with