diff options
| author | herbelin | 2001-09-25 11:51:53 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-25 11:51:53 +0000 |
| commit | d3822832501ffac6507b026e225bc2906419800e (patch) | |
| tree | 88dd0bc1e80e383433305f7d2aa2ee652d59ce70 | |
| parent | e79b91f4753385fa87ddcb62cba4a013629bfd60 (diff) | |
Qqes oublis
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2068 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | ANNONCE | 12 | ||||
| -rw-r--r-- | CHANGES | 21 |
2 files changed, 22 insertions, 11 deletions
@@ -4,13 +4,17 @@ on version 7.0. The main features of Coq versions 7.0 and 7.1 over version 6.3.1 are - - a primitive let-in construct + - new primitive let-in construct - qualified names - - a new high-level tactic language + - new high-level tactic language - improved search facilities - - a new extraction algorithm managing the Type level + - new rewriting tactic for types equipped with specific equalities + - new tactic Field to decide equalities on commutative fields + - new tactic Fourier to solve linear inequalities on reals numbers + - new tactics for induction/case analysis in "natural" style + - 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) + - deep restructuration of the code (safer, simpler and more efficient) Compared to version 7.0, the new version provides with @@ -11,13 +11,20 @@ Notes: Main novelties ============== -- new primitive let-in construct -- long names -- new high-level tactic language -- improved search facilities -- new extraction algorithm managing the Type level -- export of theories to XML for publishing and rendering purposes -- deep restructuration of the code (safer, simpler and more efficient) +References are to Coq V7.1 reference manual + +- New primitive let-in construct (see section 1.2.8) +- Long names (see section 2.6) +- New high-level tactic language (see chapter 10) +- Improved search facilities (see section 5.2) +- New extraction algorithm managing the Type level (see chapter 17) +- New rewriting tactic for arbitrary equalities (see chapter 19) +- New tactic Field to decide equalities on commutative fields (see 7.11) +- New tactic Fourier to solve linear inequalities on reals numbers (see 7.11) +- New tactics for induction/case analysis in "natural" style (see 7.7) +- Deep restructuration of the code (safer, simpler and more efficient) +- Export of theories to XML for publishing and rendering purposes + (see http://www.cs.unibo.it/helm) Details of changes |