diff options
| author | herbelin | 2012-04-15 22:06:06 +0000 |
|---|---|---|
| committer | herbelin | 2012-04-15 22:06:06 +0000 |
| commit | 25c1cfeea010b7267955d6683a381b50e2f52f71 (patch) | |
| tree | f88cbc7fc24704851c5729487a85d55dd33d3692 | |
| parent | 001a56de3c85c1134e5901f23f6a4b8bb826518c (diff) | |
Update CHANGES
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15179 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | CHANGES | 10 |
1 files changed, 5 insertions, 5 deletions
@@ -15,8 +15,8 @@ Notations - "Bind Scope" can no longer bind "Funclass" and "Sortclass". -Changes from V8.4beta to V8.4 -============================= +Changes from V8.4beta to V8.4beta2 +================================== Vernacular commands @@ -44,15 +44,15 @@ Tactics Libraries -- MSetRBT : a new implementation of MSets via Red-Black trees (initial +- MSetRBT: a new implementation of MSets via Red-Black trees (initial contribution by Andrew Appel). -- MSetAVL : for maximal sharing with the new MSetRBT, the argument order +- MSetAVL: for maximal sharing with the new MSetRBT, the argument order of Node has changed (this should be transparent to regular MSets users). Module System - The names of modules (and module types) are now in a fully separated - namespace from ordinary definitions : "Definition E:=0. Module E. End E." + namespace from ordinary definitions: "Definition E:=0. Module E. End E." is now accepted. CoqIDE |