diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-26 14:16:26 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-26 14:16:26 +0000 |
| commit | 46f7f0bc4a1cb1a403d414ecec23273a5becd236 (patch) | |
| tree | 3d966a0246cc3644b5d109511ca67f8cda33dc07 /CHANGES | |
| parent | 20cd48548993657579ed3e49bcb5457b767ef77c (diff) | |
Suppression des parseurs et printeurs v7; suppression du traducteur; changements collatéraux
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7737 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 3 |
1 files changed, 2 insertions, 1 deletions
@@ -3,7 +3,7 @@ Changes from V8.0 Syntax -- Removal of old syntax and translation support +- No more support for version 7 syntax and for translation to version 8 syntax. Environment variables @@ -79,6 +79,7 @@ Library compatibility (useless hypothesys of Zgt_square_simpl and Zlt_square_simpl removed; fixed names mentioning letter O instead of digit 0; weaken premises in Z_lt_induction) +- Change of the internal names of lemmas in OmegaLemmas Tools |