Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof

eg ![proof] becomes STATE proof

This commits still supports the old ![]
so there is redundancy:
~~~
VERNAC EXTEND Foo STATE proof
| ...

VERNAC EXTEND Foo
| ![proof] ...
~~~
with the ![] form being local to the rule and the STATE form
applying to the whole EXTEND except for the rules with a ![].

6 files changed, 24 insertions, 24 deletions

diff --git a/plugins/derive/g_derive.mlg b/plugins/derive/g_derive.mlg
index d25b8fd01c..526989fdf3 100644
--- a/plugins/derive/g_derive.mlg
+++ b/plugins/derive/g_derive.mlg
@@ -22,7 +22,7 @@ let classify_derive_command _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpac
 
 }
 
-VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command }
-| ![ open_proof ] [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
+VERNAC COMMAND EXTEND Derive CLASSIFIED BY { classify_derive_command } STATE open_proof
+| [ "Derive" ident(f) "SuchThat" constr(suchthat) "As" ident(lemma) ] ->
   { Derive.(start_deriving f suchthat lemma) }
 END
diff --git a/plugins/extraction/g_extraction.mlg b/plugins/extraction/g_extraction.mlg
index 487accbc9b..9ea3fbeaf4 100644
--- a/plugins/extraction/g_extraction.mlg
+++ b/plugins/extraction/g_extraction.mlg
@@ -177,7 +177,7 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
 END
 (* Show the extraction of the current proof *)
 
-VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
-| ![ proof_query ] [ "Show" "Extraction" ]
+VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY STATE proof_query
+| [ "Show" "Extraction" ]
   -> { show_extraction }
 END
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index cc772e96f3..8c9b1e7ba4 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -176,8 +176,8 @@ let () =
 }
 
 (* TASSI: n'importe quoi ! *)
-VERNAC COMMAND EXTEND Function
-| ![ maybe_open_proof ] ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+VERNAC COMMAND EXTEND Function STATE maybe_open_proof
+| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
     => { let hard = List.exists (function
            | _,((_,(Some { CAst.v = CMeasureRec _ }
              | Some { CAst.v = CWfRec _}),_,_,_),_) -> true
@@ -224,8 +224,8 @@ let warning_error names e =
 
 }
 
-VERNAC COMMAND EXTEND NewFunctionalScheme
-| ![ maybe_open_proof ] ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+VERNAC COMMAND EXTEND NewFunctionalScheme STATE maybe_open_proof
+| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
    => { Vernacextend.(VtSideff(List.map pi1 fas), VtLater) }
    ->
     { begin
@@ -263,7 +263,7 @@ VERNAC COMMAND EXTEND NewFunctionalCase
 END
 
 (***** debug only ***)
-VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-| ![ maybe_open_proof ] ["Generate" "graph" "for" reference(c)] ->
+VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY STATE maybe_open_proof
+| ["Generate" "graph" "for" reference(c)] ->
   { make_graph (Smartlocate.global_with_alias c) }
 END
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 4a2fb425ac..0ded60d9c7 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -931,8 +931,8 @@ END
 (* spiwack: I put it in extratactics because it is somewhat tied with
    the semantics of the LCF-style tactics, hence with the classic tactic
    mode. *)
-VERNAC COMMAND EXTEND GrabEvars
-| ![ proof ] [ "Grab" "Existential" "Variables" ]
+VERNAC COMMAND EXTEND GrabEvars STATE proof
+| [ "Grab" "Existential" "Variables" ]
   => { classify_as_proofstep }
   -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.V82.grab_evars p) pstate }
 END
@@ -963,8 +963,8 @@ TACTIC EXTEND unshelve
 END
 
 (* Command to add every unshelved variables to the focus *)
-VERNAC COMMAND EXTEND Unshelve
-| ![ proof ] [ "Unshelve" ]
+VERNAC COMMAND EXTEND Unshelve STATE proof
+| [ "Unshelve" ]
   => { classify_as_proofstep }
   -> { fun ~pstate -> Proof_global.modify_proof (fun p  -> Proof.unshelve p) pstate  }
 END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 9bf5bd1bda..960e5b76f8 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -434,13 +434,13 @@ let is_explicit_terminator = function TacSolve _ -> true | _ -> false
 
 }
 
-VERNAC { tactic_mode } EXTEND VernacSolve
-| ![ proof ] [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+VERNAC { tactic_mode } EXTEND VernacSolve STATE proof
+| [ ltac_selector_opt(g) ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     { classify_as_proofstep } -> {
     let g = Option.default (Goal_select.get_default_goal_selector ()) g in
     vernac_solve g n t def
   }
-| ![ proof ] [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
+| [ "par" ":" ltac_info_opt(n) tactic(t) ltac_use_default(def) ] =>
     {
       let anon_abstracting_tac = is_anonymous_abstract t in
       let solving_tac = is_explicit_terminator t in
diff --git a/plugins/ltac/g_obligations.mlg b/plugins/ltac/g_obligations.mlg
index c01b97c14d..58c8dabd79 100644
--- a/plugins/ltac/g_obligations.mlg
+++ b/plugins/ltac/g_obligations.mlg
@@ -87,18 +87,18 @@ let classify_obbl _ = Vernacextend.(VtStartProof (Doesn'tGuaranteeOpacity,[]), V
 
 }
 
-VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl }
-| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
+VERNAC COMMAND EXTEND Obligations CLASSIFIED BY { classify_obbl } STATE open_proof
+| [ "Obligation" integer(num) "of" ident(name) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, Some name, Some t) tac }
-| ![ open_proof ] [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
+| [ "Obligation" integer(num) "of" ident(name) withtac(tac) ] ->
     { obligation (num, Some name, None) tac }
-| ![ open_proof ] [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
+| [ "Obligation" integer(num) ":" lglob(t) withtac(tac) ] ->
     { obligation (num, None, Some t) tac }
-| ![ open_proof ] [ "Obligation" integer(num) withtac(tac) ] ->
+| [ "Obligation" integer(num) withtac(tac) ] ->
     { obligation (num, None, None) tac }
-| ![ open_proof ] [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
+| [ "Next" "Obligation" "of" ident(name) withtac(tac) ] ->
     { next_obligation (Some name) tac }
-| ![ open_proof ] [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
+| [ "Next" "Obligation" withtac(tac) ] -> { next_obligation None tac }
 END
 
 VERNAC COMMAND EXTEND Solve_Obligation CLASSIFIED AS SIDEFF