diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-21 10:51:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-01-21 10:51:16 +0000 |
| commit | 98960d29e3073ab5f2a2f77a4b3c21cc2935ba67 (patch) | |
| tree | 4aa712495ce4656bb25cbc696560ba31e4458dc0 /CHANGES | |
| parent | 809098b2ba18a410310c6e9643193543f7386799 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5224 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 16 |
1 files changed, 12 insertions, 4 deletions
@@ -1,5 +1,13 @@ -Changes from V8.0 old syntax to V8.0 -==================================== +Changes from V8.0beta to V8.0 +============================= + +Bug fixes + +- Translator printing bug of reals fixed +- Obsolete "Implicit Arguments On/Off" removed + +Changes from V8.0beta old syntax to V8.0beta +============================================ New concrete syntax @@ -74,8 +82,8 @@ Known problems of the automatic translation annotations are eta-reduced predicates -Changes from V7.4 to V8.0 old syntax -==================================== +Changes from V7.4 to V8.0beta old syntax +======================================== Logic |