diff options
Diffstat (limited to 'dev')
| -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 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]. |