Merge PR #12229: Hopefully consensual cleaning of keywords

Reviewed-by: Zimmi48
Reviewed-by: jfehrle
Ack-by: ppedrot

11 files changed, 55 insertions, 47 deletions

diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst
index acdd4408ed..899173a83a 100644
--- a/doc/sphinx/language/coq-library.rst
+++ b/doc/sphinx/language/coq-library.rst
@@ -9,11 +9,11 @@ The |Coq| library
 
 The |Coq| library has two parts:
 
-  * **The basic library**: definitions and theorems for
+  * The :gdef:`prelude`: definitions and theorems for
     the most commonly used elementary logical notions and
     data types. |Coq| normally loads these files automatically when it starts.
 
-  * **The standard library**: general-purpose libraries with
+  * The :gdef:`standard library`: general-purpose libraries with
     definitions and theorems for sets, lists, sorting,
     arithmetic, etc. To use these files, users must load them explicitly
     with the ``Require`` command (see :ref:`compiled-files`)
@@ -28,8 +28,8 @@ also be browsed at http://coq.inria.fr/stdlib/.
 
 
 
-The basic library
------------------
+The prelude
+-----------
 
 This section lists the basic notions and results which are directly
 available in the standard |Coq| system. Most of these constructions
diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst
index 9473cc5a15..aa93b4d21f 100644
--- a/doc/sphinx/language/core/basic.rst
+++ b/doc/sphinx/language/core/basic.rst
@@ -130,30 +130,37 @@ Strings
   identified with :production:`string`.
 
 Keywords
-  The following character sequences are reserved keywords that cannot be
-  used as identifiers::
+  The following character sequences are keywords defined in the main Coq grammar
+  that cannot be used as identifiers (even when starting Coq with the `-noinit`
+  command-line flag)::
 
     _ 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.
+  The following are keywords defined in notations or plugins loaded in the :term:`prelude`::
 
-Other tokens
-  The set of
-  tokens defined at any given time can vary because the :cmd:`Notation`
-  command can define new tokens.  A :cmd:`Require` command may load more notation definitions,
-  while the end of a :cmd:`Section` may remove notations.  Some notations
-  are defined in the standard library (see :ref:`thecoqlibrary`) and are generally
-  loaded automatically at startup time.
+    IF by exists exists2 using
+
+  Note that loading additional modules or plugins may expand the set of reserved
+  keywords.
 
-  Here are the character sequences that |Coq| directly defines as tokens
-  without using :cmd:`Notation`::
+Other tokens
+  The following character sequences are tokens defined in the main Coq grammar
+  (even when starting Coq with the `-noinit` command-line flag)::
 
-    ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - ->
+    ! #[ % & ' ( () ) * + , - ->
     . .( .. ... / : ::= := :> :>> ; < <+ <- <:
-    <<: <= = => > >-> >= ? @ @{ [ [= ] _
-    `( `{ { {| | |- || }
+    <<: <= = => > >-> >= ? @ @{ [ ] _
+    `( `{ { {| | }
+
+  The following character sequences are tokens defined in notations or plugins
+  loaded in the :term:`prelude`::
+
+    ** [= |- || ->
+
+  Note that loading additional modules or plugins may expand the set of defined
+  tokens.
 
   When multiple tokens match the beginning of a sequence of characters,
   the longest matching token is used.
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index b184311bef..90173d65bf 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -57,6 +57,8 @@ mode but it can also be used in toplevel definitions as shown below.
 
 .. note::
 
+   - The grammar reserves the token ``||``.
+
    - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative.
 
      .. example::
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 439f7fb9f6..127e4c6dbe 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -36,6 +36,18 @@ language will be described in Chapter :ref:`ltac`.
 Common elements of tactics
 --------------------------
 
+Reserved keywords
+~~~~~~~~~~~~~~~~~
+
+The tactics described in this chapter reserve the following keywords::
+
+  by using
+
+Thus, these keywords cannot be used as identifiers. It also declares
+the following character sequences as tokens::
+
+  ** [= |-
+
 .. _invocation-of-tactics:
 
 Invocation of tactics
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index 963f029766..c19dd00b38 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -26,16 +26,6 @@ open Pcoq.Constr
 (* TODO: avoid this redefinition without an extra dep to Notation_ops *)
 let ldots_var = Id.of_string ".."
 
-let constr_kw =
-  [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for";
-    "end"; "as"; "let"; "if"; "then"; "else"; "return";
-    "SProp"; "Prop"; "Set"; "Type";
-    ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>";
-    ".("; "()"; "`{"; "`("; "@{"; "{|";
-    "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ]
-
-let _ = List.iter CLexer.add_keyword constr_kw
-
 let mk_cast = function
     (c,(_,None)) -> c
   | (c,(_,Some ty)) ->
diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg
index 7cabd850ad..cc59b2175b 100644
--- a/parsing/g_prim.mlg
+++ b/parsing/g_prim.mlg
@@ -15,10 +15,6 @@ open Libnames
 
 open Pcoq.Prim
 
-let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"]
-let _ = List.iter CLexer.add_keyword prim_kw
-
-
 let local_make_qualid loc l id = make_qualid ~loc (DirPath.make l) id
 
 let my_int_of_string ?loc s =
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/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index aef5f645f4..0e661543db 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -216,8 +216,8 @@ GRAMMAR EXTEND Gram
   ;
   match_key:
     [ [ "match" -> { Once }
-      | "lazymatch" -> { Select }
-      | "multimatch" -> { General } ] ]
+      | IDENT "lazymatch" -> { Select }
+      | IDENT "multimatch" -> { General } ] ]
   ;
   input_fun:
     [ [ "_" -> { Name.Anonymous }
diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg
index 6a158bde17..e51b1f051d 100644
--- a/plugins/ltac/g_tactic.mlg
+++ b/plugins/ltac/g_tactic.mlg
@@ -30,9 +30,6 @@ open Pcoq
 
 let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta]
 
-let tactic_kw = [ "->"; "<-" ; "by" ]
-let _ = List.iter CLexer.add_keyword tactic_kw
-
 let err () = raise Stream.Failure
 
 (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg
index 058fa691ee..80a4de472c 100644
--- a/vernac/g_proofs.mlg
+++ b/vernac/g_proofs.mlg
@@ -97,7 +97,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) }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 049c3a0844..42259cee10 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -30,9 +30,6 @@ open Pcoq.Module
 open Pvernac.Vernac_
 open Attributes
 
-let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:"; "where"; "at" ]
-let _ = List.iter CLexer.add_keyword vernac_kw
-
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)