From 3cfc37893674f06a91c01ab51d0605cedb906a9a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 13 Dec 2003 18:27:29 +0000
Subject: MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5095 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/translate.txt | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

(limited to 'dev')

diff --git a/dev/translate.txt b/dev/translate.txt
index a7d9aabdef..5b372c96c3 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
 ----------------------------
-- 
cgit v1.2.3