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.
---
 vernac/g_proofs.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/g_proofs.mlg')

diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 60ff9896bf..5b80ed6794 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -56,7 +56,7 @@ GRAMMAR EXTEND Gram
     [ [ IDENT "Goal"; c = lconstr ->
         { VernacDefinition (Decls.(NoDischarge, Definition), ((CAst.make ~loc Names.Anonymous), None), ProveBody ([], c)) }
       | IDENT "Proof" -> { VernacProof (None,None) }
-      | IDENT "Proof"; "using"; l = G_vernac.section_subset_expr ->
+      | IDENT "Proof"; IDENT "using"; l = G_vernac.section_subset_expr ->
           { VernacProof (None,Some l) }
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn }
       | IDENT "Proof"; c = lconstr -> { VernacExactProof c }
-- 
cgit v1.2.3