*** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3767 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 9 deletions

diff --git a/ide/FAQ b/ide/FAQ
index a410dbe64..e6e022973 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -19,24 +19,33 @@ Q3) How to enable antialiased fonts?
 R3) Set the GDK_USE_XFT variable to 1.
 
 Q4) How can use Forall and Exists pretty symbols ?
-R4) Thanks to the Notation features in Coq, you just need to paste these
+R4) Thanks to the Notation features in Coq, you just need to insert these
 	lines in your Coq Buffer :
 ======================================================================
 Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10).
-Notation "~ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
+Notation "∃ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10).
 ======================================================================
-Then you need an input method for these symbols.
--First solution : type "<CONTROL>2200" to enter a forall. 2200 is the 
-	hexadecimal code for forall in unicode charts.
-	2203 is for exists. See http://www.unicode.org for more.
+Copy/Paste might not work. You need to load a file containing these lines or to enter 
+the "∀" using an input method. As a convenience, you may put these lines in
+a utf8.v file and start coqide with : 
+	coqide -l utf8.v
+
 
--Second solution : rebind "<AltGr>a" to forall. Under X11, you need to 
-	use 
+Input Methods:
+-First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow. 
+	2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀"	
+	in UTF-8.
+	2203 is for exists. See http://www.unicode.org for more.
+-Second solution : rebind "<AltGr>a" to forall and "<AltGr>e" to exists. Under X11, you need to 
+	use something like
 		xmodmap -e "keycode  24 = a A F13 F13" 
+		xmodmap -e "keycode  26 = e E F14 F14" 
 	and then to add   
 		bind "F13" {"insert-at-cursor" ("∀")}
+		bind "F14" {"insert-at-cursor" ("∃")}
 	to your "binding "text"" section in .coqiderc. 
 	The strange ("∀") argument is the UTF-8 encoding for
 	0x2200. It is computed by lablgtk2 by 
 		Glib.Utf8.from_unichar 0x2200;;
-	Further symbols can be found on higher Fxx key symbols.
+	Further symbols can be bound on higher Fxx key symbols.
+