coqide: toolbar/autosave

Hugo: Suppression du type dans les notations == et <> entre
Suppression du type dans les notations == et <> entre
volution second traducteur selon discussion  TYPES


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

1 files changed, 25 insertions, 14 deletions

diff --git a/ide/FAQ b/ide/FAQ
index e00131f7b4..ba97211e57 100644
--- a/ide/FAQ
+++ b/ide/FAQ
@@ -1,36 +1,38 @@
+			CoqIde FAQ
+
+Q0) What is CoqIde?
+R0: A powerfull graphical interface for Coq. See http://coq.inria.fr. for more informations
+
 Q1) How to enable Emacs keybindings?
 R1: Insert 
 	gtk-key-theme-name = "Emacs"
     in your ".coqide-gtk2rc" file. It may be in the current dir
     or in $HOME dir. This is done by default.
 
-
 Q2) How to enable antialiased fonts?
 R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2.
-    If some of your fonts seem not to be available, set to 0.
+    If some of your fonts are not available, set GDK_USE_XFT to 0.
 
-Q4) How can use Forall and Exists pretty symbols ?
+Q4) How to use those Forall and Exists pretty symbols?
 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).
 ======================================================================
-Copy/Paste from this file will not work. 
+Copy/Paste of these lines from this file will not work outside of CoqIde.
 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
+using an input method (see Q5). As a convenience, you may put these lines in
 a utf8.v file and start coqide with : 
 	coqide -l utf8.v
-In the ide subdir of Coq sources, you will find a sample utf8.v with some 
-notations
-
+In the ide subdir of Coq library, you will find a sample utf8.v with some 
+pretty notations.
 
-
-Input Methods:
--First solution : type "<CONTROL><SHIFT>2200" to enter a forall in the script widow. 
+Q5) How to define an input method for non ASCII symbols?
+R5)-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.
+	2203 is for exists. See http://www.unicode.org for more codes.
 -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" 
@@ -40,7 +42,16 @@ Input Methods:
 		bind "F14" {"insert-at-cursor" ("∃")}
 	to your "binding "text"" section in .coqiderc-gtk2rc.
 	The strange ("∀") argument is the UTF-8 encoding for
-	0x2200. It is computed by lablgtk2 by 
+	0x2200. 
+	You can compute these encodings using the lablgtk2 toplevel with 
 		Glib.Utf8.from_unichar 0x2200;;
-	Further symbols can be bound on higher Fxx key symbols.
+	Further symbols can be bound on higher Fxx keys or on even on other keys you
+	do not need .
+
+Q6) How to build a custom CoqIde with user ml code?
+R6) Use 
+	coqmktop -ide -byte m1.cmo...mi.cmo
+    or 
+	coqmktop -ide -opt m1.cmx...mi.cmx
+