diff options
| author | herbelin | 2001-09-25 07:30:49 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-25 07:30:49 +0000 |
| commit | f5c0396f5ff4a1357f954fccd725ca68e40bd62c (patch) | |
| tree | ee821bb98beb9da6bbf87985d53b1253634f07a5 /ANNONCE | |
| parent | c2c9de4b427f56e9e931239d95d27a8a3592539e (diff) | |
Mise en page
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2063 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ANNONCE')
| -rw-r--r-- | ANNONCE | 10 |
1 files changed, 6 insertions, 4 deletions
@@ -6,9 +6,9 @@ on version 7.0. - a primitive let-in construct - qualified names - - library structuration - - a high-level tactic language + - a new high-level tactic language - improved search facilities + - a new extraction algorithm managing the Type level - export of theories to XML for publishing and rendering purposes - a deep restructuration of the code (safer, simpler and more efficient) @@ -26,9 +26,10 @@ on version 7.0. - new tactics NewDestruct, NewInduction and Assert intended to improve the behaviour of previous Elim and Induction, Case and Destruct, and Cut tactics - - known-bugs fixes + - known-bugs fixed - excessive memory use mainly fixed + The Realizer/Program tactics are not available in Coq V7.1. The Correctness command can be used instead. @@ -52,5 +53,6 @@ list of changes including sources of incompatibilities. and to mail Coq-Club@pauillac.inria.fr for general questions or remarks (moderated). - The Coq development team (in LogiCal team) + + The Coq development team |