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 ![].

1 files changed, 4 insertions, 4 deletions

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