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 || --- doc/sphinx/language/core/basic.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'doc') 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. -- cgit v1.2.3 From 259162be000a8a66bf4f551be64d6a5d61edce05 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Nov 2019 18:19:44 +0100 Subject: Mention keywords used in tactics from g_tactic.mlg. --- doc/sphinx/proof-engine/tactics.rst | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8989dd29ab..78ac7d00dd 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 -- cgit v1.2.3 From 986bfd1ff69231f1b17efda2fa5d13b88a39caee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Nov 2019 20:54:52 +0100 Subject: Mention keywords from g_ltac.mlg used in Ltac. --- doc/sphinx/proof-engine/ltac.rst | 3 +++ 1 file changed, 3 insertions(+) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b184311bef..dc994fe863 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,6 +57,9 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: + - The grammar reserves the keywords ``lazymatch`` and + ``multimatch`` as well as the token ``||``. + - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative. .. example:: -- cgit v1.2.3 From 20f0e2efb87541e511cf31e220a44e4376c44550 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 2 May 2020 23:22:48 +0200 Subject: Moving lazymatch and multimatch to simple identifiers. --- doc/sphinx/proof-engine/ltac.rst | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'doc') diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc994fe863..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,8 +57,7 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: - - The grammar reserves the keywords ``lazymatch`` and - ``multimatch`` as well as the token ``||``. + - The grammar reserves the token ``||``. - The infix tacticals  ``… || …`` ,  ``… + …`` , and  ``… ; …``  are associative. -- cgit v1.2.3 From 037c8d299ca1a5aef9813133dca07ad6f35e1e75 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 6 May 2020 16:59:19 +0200 Subject: Keywords: Applying suggestions from Jim Fehrle and Théo Zimmermann. --- doc/sphinx/language/coq-library.rst | 8 ++++---- doc/sphinx/language/core/basic.rst | 31 +++++++++++++++++++------------ 2 files changed, 23 insertions(+), 16 deletions(-) (limited to 'doc') 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 3940242bb3..aa93b4d21f 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -130,31 +130,38 @@ 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 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):: ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: <<: <= = => > >-> >= ? @ @{ [ ] _ `( `{ { {| | } + 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. Occasionally you may need to insert spaces to separate tokens. For example, -- cgit v1.2.3