From 02fda88fc065577f3f9604477db2e03eb4d5a9b4 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 7 May 2019 14:34:06 +0200
Subject: 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 ![].
---
 plugins/funind/g_indfun.mlg | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/funind')

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
-- 
cgit v1.2.3