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/extraction/g_extraction.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction')

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