From 3fa2430e8c66408fa3a8fe95af54e53d20e5951b Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 10 Nov 2020 15:57:02 +0100
Subject: Add support for Proof using in -noinit mode.

"Proof with" is Ltac-specific but there is no reason why it should be
the same for "Proof using".
---
 plugins/ltac/g_ltac.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c54f8ffa78..bd46e24a1c 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -332,8 +332,8 @@ GRAMMAR EXTEND Gram
         l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
           { Vernacexpr.VernacProof (Some (in_tac ta), l) }
       | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
-        ta = OPT [ "with"; ta = Pltac.tactic -> { in_tac ta } ] ->
-          { Vernacexpr.VernacProof (ta,Some l) } ] ]
+        "with"; ta = Pltac.tactic ->
+          { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ]
   ;
   hint:
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
-- 
cgit v1.2.3


From 1117058b39603bb42591961f4b13faa6c58c6ee2 Mon Sep 17 00:00:00 2001
From: Théo Zimmermann
Date: Tue, 10 Nov 2020 16:02:56 +0100
Subject: Revert to "using" not being a keyword in -noinit mode.

The IDENT annotations in g_ltac.mlg are required to not break the
parser.
---
 plugins/ltac/g_ltac.mlg | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index bd46e24a1c..c2e95c45f9 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -329,9 +329,9 @@ GRAMMAR EXTEND Gram
   ;
   command:
     [ [ IDENT "Proof"; "with"; ta = Pltac.tactic;
-        l = OPT [ "using"; l = G_vernac.section_subset_expr -> { l } ] ->
+        l = OPT [ IDENT "using"; l = G_vernac.section_subset_expr -> { l } ] ->
           { Vernacexpr.VernacProof (Some (in_tac ta), l) }
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr;
+      | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr;
         "with"; ta = Pltac.tactic ->
           { Vernacexpr.VernacProof (Some (in_tac ta),Some l) } ] ]
   ;
-- 
cgit v1.2.3