diff options
| author | Gaëtan Gilbert | 2019-02-07 13:32:38 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-02-12 17:16:39 +0100 |
| commit | 2419d4539f469214b73c2c8f6d8fe2a6ccdfdb88 (patch) | |
| tree | 2abf3466449dc540a3471f81c91d4e79ce60e019 | |
| parent | aeb5deb414daf47e0f766489742b4ef9c2529c63 (diff) | |
Fix failing coqtops in coqide.rst
| -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 |