MAJ

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

1 files changed, 18 insertions, 0 deletions

diff --git a/dev/translate.txt b/dev/translate.txt
index a7d9aabde..5b372c96c 100644
--- a/dev/translate.txt
+++ b/dev/translate.txt
@@ -9,6 +9,17 @@ The translator is a smart, robust and powerful tool to improve the
 readibility of your script. The current document describes the
 possibilities of the translator.
 
+In case of problem recompiling the translated files, don't waste time
+to modify the translated file by hand, read first the following
+document telling on how to modify the original files to get a smooth
+uniform safe translation. All 60000 lines of Coq lines on our
+user-contributions server have been translated without any change
+afterwards, and 0,5 % of the lines of the original files (mainly
+notations) had to be modified beforehand to get this result.
+
+Table of contents
+-----------------
+
 I) Implicit Arguments
  1) Strict Implicit Arguments 
  2) Implicit Arguments in standard library
@@ -32,6 +43,7 @@ III) Various pitfalls
  1) New keywords
  2) Old "Case" and "Match"
  3) Change of definition or theorem names
+ 4) Change of tactic names
 
 ---------------------------------------------------------------------
 
@@ -322,6 +334,12 @@ are systematically qualified even tough it may not be necessary.  The
 same apply for names "GREATER", "EQUAL", "LESS", etc... [COMPLETE LIST
 TO GIVE].
 
+4) Change of tactics names
+
+  Since tactics names are now lowercase, this can clash with
+user-defined tactic definitions. To pally this, clashing names are
+renamed by adding an extra "_" to their name.
+
 ======================================================================
 Main examples for new syntax
 ----------------------------