From 62f6fb862ce4f3eec46200d11e503aa5d6d051db Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Nov 2019 17:18:06 +0100
Subject: Documenting plugin/tactic/stdlib keywords in corresponding chapters.

Incidentally removing "discriminated", "(bfs)" and "(dfs)" from
keywords. It is enough to make them normal identifiers.

Note:
- keywords reserved by the tactics are: ** [= _eqn |- by using
- keywords reserved by ltac are: lazymatch multimatch ||
---
 vernac/g_proofs.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index e84fce5504..f2a1dce01d 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -98,7 +98,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Guarded" -> { VernacCheckGuard }
       (* Hints for Auto and EAuto *)
       | IDENT "Create"; IDENT "HintDb" ;
-          id = IDENT ; b = [ "discriminated" -> { true } | -> { false } ] ->
+          id = IDENT ; b = [ IDENT "discriminated" -> { true } | -> { false } ] ->
             { VernacCreateHintDb (id, b) }
       | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases ->
           { VernacRemoveHints (dbnames, ids) }
-- 
cgit v1.2.3