Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous Coqide

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

2 files changed, 23 insertions, 0 deletions

diff --git a/INSTALL.ide b/INSTALL.ide
index 029ec03ce7..5a4a622386 100644
--- a/INSTALL.ide
+++ b/INSTALL.ide
@@ -115,3 +115,17 @@ There are three configuration files located in your $(HOME) dir.
   to change the default shortcuts for the menus.
 
 Read ide/FAQ for more informations.
+
+
+TROUBLESHOOTING
+
+  - Problem with automatic templates
+
+    Some users may experiment problems with unwanted automatic
+    templates while using Coqide. This is due to a change in the
+    modifiers keys available through GTK. The straightest way to get
+    rid of the problem is to edit by hand your .coqiderc (either
+    /home/<user>/.coqiderc under Linux, or 
+    C:\Documents and Settings\<user>\.coqiderc under Windows) 
+    and replace any occurence of MOD4 by MOD1.
+
diff --git a/doc/faq/FAQ.tex b/doc/faq/FAQ.tex
index f40c28c4d4..0644cf369a 100644
--- a/doc/faq/FAQ.tex
+++ b/doc/faq/FAQ.tex
@@ -2350,6 +2350,15 @@ Glib.Utf8.from_unichar 0x2200;;
  The number between braces is the hexadecimal UNICODE index for the
   missing character.
     
+\Question{How to get rid of annoying unwanted automatic templates?}
+
+Some users may experiment problems with unwanted automatic
+templates while using Coqide. This is due to a change in the
+modifiers keys available through GTK. The straightest way to get
+rid of the problem is to edit by hand your .coqiderc (either
+\verb|/home/<user>/.coqiderc| under Linux, or \\
+\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows) 
+    and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.