[vernac] Refactor Vernacular Control Attributes into a list

We place control attributes on their own, datatype, similarly to
regular attributes.

This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.

1 files changed, 9 insertions, 30 deletions

diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 747998c6cc..903a28e953 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,47 +13,26 @@
 
 open Vernacexpr
 
-let rec under_control v = v |> CAst.with_val (function
-  | VernacExpr (_, c) -> c
-  | VernacRedirect (_,c)
-  | VernacTime (_,c)
-  | VernacFail c
-  | VernacTimeout (_,c) -> under_control c
-  )
-
-let rec has_Fail v = v |> CAst.with_val (function
-  | VernacExpr _ -> false
-  | VernacRedirect (_,c)
-  | VernacTime (_,c)
-  | VernacTimeout (_,c) -> has_Fail c
-  | VernacFail _ -> true)
+(* Does this vernacular involve Fail? *)
+let has_Fail { CAst.v } = List.mem ControlFail v.control
 
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let is_navigation_vernac_expr = function
+let is_navigation_vernac = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBack _ -> true
   | _ -> false
 
-let is_navigation_vernac c =
-  is_navigation_vernac_expr (under_control c)
-
-let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
-  | VernacTime (_,c) -> is_deep_navigation_vernac c
-  | VernacRedirect (_, c)
-  | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
-  | VernacExpr _ -> false)
-
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = CAst.with_val (function
-  | VernacExpr ( _, VernacResetInitial)
-  | VernacExpr (_, VernacResetName _) -> true
-  | _ -> false)
+let is_reset = function
+  | VernacResetInitial
+  | VernacResetName _ -> true
+  | _ -> false
 
-let is_debug cmd = match under_control cmd with
+let is_debug = function
   | VernacSetOption (_, ["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_undo cmd = match under_control cmd with
+let is_undo = function
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false