From 2419d4539f469214b73c2c8f6d8fe2a6ccdfdb88 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 7 Feb 2019 13:32:38 +0100
Subject: Fix failing coqtops in coqide.rst

---
 doc/sphinx/practical-tools/coqide.rst | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

(limited to 'doc/sphinx/practical-tools')

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
-- 
cgit v1.2.3