From d067c2b4fecd9541a2dcad0625898beff52f7b1b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 9 Sep 2003 15:07:01 +0000
Subject: MAJ

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

(limited to 'dev')

diff --git a/dev/translate.txt b/dev/translate.txt
index 0085b35391..35a3befaa9 100644
--- a/dev/translate.txt
+++ b/dev/translate.txt
@@ -207,6 +207,14 @@ ML-style notation as follows
 
   Inductive and (A B:Prop) : Prop as "A /\ B" := conj (a:A) (b:B).
   
+IV) Pitfalls
+
+  Type "entier" from fast_integer.v is renamed into "N" by the
+translator. As a consequence, user-defined objects of same name "N"
+can be hidden by the new "N" if the "Require ZArith" is not done soon
+enough. The solution is to move the "Require ZArith" before users
+modules. The same apply for names "GREATER", "EQUAL", "LESS",
+etc... [COMPLETE LIST TO GIVE].
 
 
 
-- 
cgit v1.2.3