diff options
| author | herbelin | 2001-09-11 13:22:21 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-11 13:22:21 +0000 |
| commit | 26f0747a93e403b08a0432221a18591a91966eb0 (patch) | |
| tree | 17eaadea758296cdf2eaf405e71dc65740f2a954 | |
| parent | 34ab24625a5cb10c42b0b69a22c822bcf6c86e28 (diff) | |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1950 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 7 |
1 files changed, 7 insertions, 0 deletions
@@ -34,6 +34,13 @@ Modifications depuis la V7.0 hypothèses du contexte, la stratégie de nommage est différente). Elim et Case restent nécessaires pour les cas où l'hypothèse d'élimination est un produit sur un type inductif. +- Nouvelles contribs: + - CtlTctl et RailroadCrossing (Carlos Daniel Luna) [Montevideo], + - GRAPHS-BASICS (J. Duprat) [Lyon], + - FTA (Herman Geuvers et al) [Nijmegen], + - Bresenham (JCF), Diff (JCF) et PAutomata (Paulin/Freund) [Orsay], + - Functions_in_ZFC (C. Simpson), Buchberger (L. Thery), Rsa + (L. Thery) et Stalmarck (L.Thery, P. Letouzey) [Sophia] Différences oubliées dans la V7.0beta : |