diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:07:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-09 15:07:01 +0000 |
| commit | d067c2b4fecd9541a2dcad0625898beff52f7b1b (patch) | |
| tree | 8c1faec0a0f4ee38edec70ca3af87edfb39bc07d | |
| parent | a580a7a07da8651887c6fb386bd9af55bbe673a2 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4337 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | dev/translate.txt | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/dev/translate.txt b/dev/translate.txt index 0085b3539..35a3befaa 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]. |