aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-04-17 08:09:49 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2004-04-17 08:09:49 +0000
commit4766086002931e5b45d768d10bd430c7abdb5b13 (patch)
tree9492552da53b7218962e2485dfd2b2f765b265a1 /CHANGES
parent715e002ab56561fc3ecd5fc922459a9e9a8001b0 (diff)
Finalement pas de liste des contributions (cela n'avait été fait que pour la 7.0)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5686 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES16
1 files changed, 0 insertions, 16 deletions
diff --git a/CHANGES b/CHANGES
index 00600f19f..e1240159d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -44,22 +44,6 @@ User contributions
- User contributions have been updated to the new syntax
-New user contributions
-
-- A modular formalization of dictionaries based on binary search trees
-- The Constructive Coq Repository at Nijmegen
-- Coqoban: playing Sokoban within Coq
-- Preliminary linear algebra from the book "Linear Algebra" by Friedberg
-- A theory of rational numbers represented as finite binary lists
-- A theory of rational numbers represented as a quotient of Z * N
-- A modular theory of finite sets as sorted lists, red-black trees or AVLs
-- Non analytic high school geometry
-- A proof of correctness of Huffman algorithm
-- A theory of squared matrices
-- Properties of Lambek calculus
-- A formalization of Coquand's proof of Higman's lemma
-- The Formal Verification of an Incremental Garbage Collector
-
Bug fixes
- Many bugs have been fixed (cf coq-bugs web page)