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