diff options
| author | Théo Zimmermann | 2019-02-13 11:49:29 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2019-02-13 11:49:29 +0100 |
| commit | 90e2fa3344cff478a2ab23c0dbbb5eab5b4668e4 (patch) | |
| tree | 7ad437364d4998e8a95ee8c0d1a1827099bd8084 /doc/sphinx/practical-tools | |
| parent | 0b0fa735dc0da5660a870053a5a5f6fd1c5e22d1 (diff) | |
| parent | d638148dc3e0220ac99761cf9f2efa8284882c41 (diff) | |
Merge PR #9553: Sphinx various fixing of failing commands
Ack-by: Zimmi48
Diffstat (limited to 'doc/sphinx/practical-tools')
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 9455228e7d..8b7fe20191 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -230,10 +230,12 @@ mathematical symbols ∀ and ∃, you may define: .. coqtop:: in - Notation "∀ x : T, P" := - (forall x : T, P) (at level 200, x ident). - Notation "∃ x : T, P" := - (exists x : T, P) (at level 200, x ident). + Notation "∀ x .. y , P" := (forall x, .. (forall y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. + Notation "∃ x .. y , P" := (exists x, .. (exists y, P) ..) + (at level 200, x binder, y binder, right associativity) + : type_scope. There exists a small set of such notations already defined, in the file `utf8.v` of Coq library, so you may enable them just by |