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 ||

3 files changed, 16 insertions, 9 deletions

diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 9473cc5a15..3940242bb3 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -134,7 +134,7 @@ Keywords
   used as identifiers::
 
     _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop
-    SProp Set Theorem Type Variable as at cofix discriminated else end
+    SProp Set Theorem Type Variable as at cofix else end
     fix for forall fun if in let match return then where with
 
   Note that notations and plugins may define additional keywords.
@@ -150,10 +150,10 @@ Other tokens
   Here are the character sequences that |Coq| directly defines as tokens
   without using :cmd:`Notation`::
 
-    ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
+    ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
-    <<: <= = => > >-> >= ? @ @{ [ [= ] _
-    `( `{ { {| | |- || }
+    <<: <= = => > >-> >= ? @ @{ [ ] _
+    `( `{ { {| | }
 
   When multiple tokens match the beginning of a sequence of characters,
   the longest matching token is used.
diff --git a/plugins/ltac/g_class.mlg b/plugins/ltac/g_class.mlg
index 0f0341f123..81e745b714 100644
--- a/plugins/ltac/g_class.mlg
+++ b/plugins/ltac/g_class.mlg
@@ -54,16 +54,23 @@ END
 
 {
 
+let pr_search_strategy_name _prc _prlc _prt = function
+  | Dfs -> Pp.str "dfs"
+  | Bfs -> Pp.str "bfs"
+
 let pr_search_strategy _prc _prlc _prt = function
-  | Some Dfs -> Pp.str "dfs"
-  | Some Bfs -> Pp.str "bfs"
+  | Some s -> pr_search_strategy_name _prc _prlc _prt s
   | None -> Pp.mt ()
 
 }
 
+ARGUMENT EXTEND eauto_search_strategy_name PRINTED BY { pr_search_strategy_name }
+| [ "bfs" ] -> { Bfs }
+| [ "dfs" ] -> { Dfs }
+END
+
 ARGUMENT EXTEND eauto_search_strategy PRINTED BY { pr_search_strategy }
-| [ "(bfs)" ] -> { Some Bfs }
-| [ "(dfs)" ] -> { Some Dfs }
+| [ "(" eauto_search_strategy_name(s) ")" ] -> { Some s }
 | [ ] -> { None }
 END
 
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) }