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

(limited to 'vernac')

diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index ebec720ce2..60ff9896bf 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -56,6 +56,8 @@ 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 ->
+          { VernacProof (None,Some l) }
       | IDENT "Proof" ; IDENT "Mode" ; mn = string -> { VernacProofMode mn }
       | IDENT "Proof"; c = lconstr -> { VernacExactProof c }
       | IDENT "Abort" -> { VernacAbort None }
-- 
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.
---
 vernac/g_proofs.mlg | 2 +-
 vernac/g_vernac.mlg | 3 ++-
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'vernac')

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 }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index f192d67624..1c80d71ea5 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -114,7 +114,8 @@ GRAMMAR EXTEND Gram
   ;
   attribute:
     [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v }
-      | "using" ; v = attr_value -> { "using", v } ]
+      (* Required because "ident" is declared a keyword when loading Ltac. *)
+      | IDENT "using" ; v = attr_value -> { "using", v } ]
     ]
   ;
   attr_value:
-- 
cgit v1.2.3