[vernac] vernac_expr no longer recursive

3 files changed, 14 insertions, 13 deletions

diff --git a/stm/proofBlockDelimiter.ml b/stm/proofBlockDelimiter.ml
index 01b5b9a01..bebc4d5d5 100644
--- a/stm/proofBlockDelimiter.ml
+++ b/stm/proofBlockDelimiter.ml
@@ -96,7 +96,7 @@ let dynamic_bullet doc { dynamic_switch = id; carry_on_data = b } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacExpr(Vernacexpr.VernacBullet (to_bullet_val b)))
+         recovery_command = Some (Vernacexpr.VernacExpr([], Vernacexpr.VernacBullet (to_bullet_val b)))
       }
   | `Not -> `Leaks
 
@@ -125,7 +125,7 @@ let dynamic_curly_brace doc { dynamic_switch = id } =
       `ValidBlock {
          base_state = id;
          goals_to_admit = focused;
-         recovery_command = Some (Vernacexpr.VernacExpr Vernacexpr.VernacEndSubproof)
+         recovery_command = Some (Vernacexpr.VernacExpr ([], Vernacexpr.VernacEndSubproof))
       }
   | `Not -> `Leaks
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 7045df0ed..5f4fe6565 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1498,7 +1498,7 @@ end = struct (* {{{ *)
           stm_vernac_interp stop
             ~proof:(pobject, terminator) st
             { verbose = false; loc; indentation = 0; strlen = 0;
-              expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) }) in
+              expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) }) in
         ignore(Future.join checked_proof);
       end;
       (* STATE: Restore the state XXX: handle exn *)
@@ -1646,7 +1646,7 @@ end = struct (* {{{ *)
       let st = Vernacstate.freeze_interp_state `No in
       ignore(stm_vernac_interp stop ~proof st
         { verbose = false; loc; indentation = 0; strlen = 0;
-          expr = VernacExpr (VernacEndProof (Proved (Opaque,None))) });
+          expr = VernacExpr ([], VernacEndProof (Proved (Opaque,None))) });
       `OK proof
       end
     with e ->
@@ -2177,7 +2177,7 @@ let collect_proof keep cur hd brkind id =
         (try
           let name, hint = name ids, get_hint_ctx loc  in
           let t, v = proof_no_using last in
-          v.expr <- VernacExpr(VernacProof(t, Some hint));
+          v.expr <- VernacExpr([], VernacProof(t, Some hint));
           `ASync (parent last,accn,name,delegate name)
         with Not_found ->
           let name = name ids in
@@ -2872,10 +2872,9 @@ let process_transaction ?(newtip=Stateid.fresh ()) ?(part_of_script=true)
             if not in_proof && Proof_global.there_are_pending_proofs () then
             begin
               let bname = VCS.mk_branch_name x in
-              let rec opacity_of_produced_term = function
+              let opacity_of_produced_term = function
                 (* This AST is ambiguous, hence we check it dynamically *)
                 | VernacInstance (false, _,_ , None, _) -> GuaranteesOpacity
-                | VernacLocal (_,e) -> opacity_of_produced_term e
                 | _ -> Doesn'tGuaranteeOpacity in
               VCS.commit id (Fork (x,bname,opacity_of_produced_term (Vernacprop.under_control x.expr),[]));
               let proof_mode = default_proof_mode () in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2fa47ba43..99b56d484 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -49,17 +49,13 @@ let declare_vernac_classifier
   classifiers := !classifiers @ [s,f]
 
 let classify_vernac e =
-  let rec static_classifier ~poly e = match e with
+  let static_classifier ~poly e = match e with
     (* Univ poly compatibility: we run it now, so that we can just
      * look at Flags in stm.ml.  Would be nicer to have the stm
      * look at the entire dag to detect this option. *)
     | ( VernacSetOption (l,_) | VernacUnsetOption l)
       when CList.equal String.equal l Vernacentries.universe_polymorphism_option_name ->
        VtSideff [], VtNow
-    (* Nested vernac exprs *)
-    | VernacProgram e -> static_classifier ~poly e
-    | VernacLocal (_,e) -> static_classifier ~poly e
-    | VernacPolymorphic (b, e) -> static_classifier ~poly:b e
     (* Qed *)
     | VernacAbort _ -> VtQed VtDrop, VtLater
     | VernacEndProof Admitted -> VtQed VtKeepAsAxiom, VtLater
@@ -193,7 +189,13 @@ let classify_vernac e =
         with Not_found -> anomaly(str"No classifier for"++spc()++str (fst s)++str".")
   in
   let rec static_control_classifier ~poly = function
-    | VernacExpr e -> static_classifier ~poly e
+    | VernacExpr (f, e) ->
+      let poly = List.fold_left (fun poly f ->
+          match f with
+          | VernacPolymorphic b -> b
+          | (VernacProgram | VernacLocal _) -> poly
+        ) poly f in
+      static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,(_,e)) | VernacRedirect (_, (_,e)) ->
        static_control_classifier ~poly e