diff options
| author | Hugo Herbelin | 2019-11-13 17:18:06 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-05-06 17:04:11 +0200 |
| commit | 62f6fb862ce4f3eec46200d11e503aa5d6d051db (patch) | |
| tree | 323b0a77e1f0dbf2e07067b65fc0f359f1d00ff2 /doc | |
| parent | bc79d319d38f766a6b7bbeb1f1071b046642089b (diff) | |
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 ||
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 8 |
1 files changed, 4 insertions, 4 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. |