aboutsummaryrefslogtreecommitdiff
path: root/CHANGES
diff options
context:
space:
mode:
authorherbelin2006-04-28 12:24:14 +0000
committerherbelin2006-04-28 12:24:14 +0000
commita184d54b95c40bc2890fc91f236bbdf983ebc83d (patch)
treed95ef613b68e96c0e7de041baae4c721bd48cd25 /CHANGES
parent11aaf97fa5f773c8a81d12255414cd3f5d189d25 (diff)
Standardisation du nom des méthodes de Evd
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8759 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES4
1 files changed, 3 insertions, 1 deletions
diff --git a/CHANGES b/CHANGES
index b094d8ffba..3f4cf0aa4c 100644
--- a/CHANGES
+++ b/CHANGES
@@ -96,9 +96,11 @@ Notations
- no more automatic printing box in case of user-provided printing "format".
- new notation "exists! x:A, P" for unique existence.
-Library
+Libraries
- Small extension of Zmin.V, new Zmax.v, new Zminmax.v
+- Reworking of the files on classical logic and description principles
+ (possible incompatibilities)
- New library on String and Ascii characters (contributed by L. Thery)
- Few other improvements in ZArith potentially exceptionally breaking the
compatibility (useless hypothesys of Zgt_square_simpl and