diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-23 07:52:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-02-23 07:52:24 +0000 |
| commit | c98c25749b0fb2383f21339aa6b67ae58e53ad42 (patch) | |
| tree | 5e57a638b61e4a2bf7ba1f64679d3e1931489678 /CHANGES | |
| parent | a533eea9dbff0c9393345b2e42a0c388ba32523d (diff) | |
Ajout 'exists! x:A, P
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8085 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 9 |
1 files changed, 5 insertions, 4 deletions
@@ -4,7 +4,7 @@ Changes from V8.0 Syntax - No more support for version 7 syntax and for translation to version 8 syntax. -- Support for primitive interpretation of string litterals +- Support for primitive interpretation of string literals - Extended support for Unicode ranges (Unicode doc TODO) Environment variables @@ -84,9 +84,10 @@ Modules Notations -- "format" option aware of recursive notations -- added insertion of spaces by default in recursive notations w/o separators -- no more automatic printing box in case of user-provided printing "format" +- "format" option aware of recursive notations. +- added insertion of spaces by default in recursive notations w/o separators. +- no more automatic printing box in case of user-provided printing "format". +- new notation "exists! x:A, P" for unique existence. Library |