diff options
author | 2000-12-25 18:59:08 +0000 | |
---|---|---|
committer | 2000-12-25 18:59:08 +0000 | |
commit | 0d294b3c91e0b93cb71d3b4ef1f00ef06ad711a6 (patch) | |
tree | d426dba76f1c0cd600deab2f9e0bf3ff7d40ce39 /ANNONCE | |
parent | 3d1e0eef2e977316e3958b4074f5bfd10f0fd420 (diff) |
MAJ
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1207 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ANNONCE')
-rw-r--r-- | ANNONCE | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -10,9 +10,9 @@ provided for users willing to experiment the new features which are: - an improved Search facilities using patterns (by Yves Bertot) - a "natural" syntax for real numbers (by Micaëla Mayero) - various bug fixes - - a command to export definitions, theorems and proofs to XML to be used with - Helm's publishing and rendering tools (see http://www.cs.unibo.it/helm) - (by Claudio Sacerdoti Coen) + - a command to export theories to XML to be used with Helm's publishing + and rendering tools (see http://www.cs.unibo.it/helm) (by Claudio + Sacerdoti Coen) Extraction and the Realizer/Program tactics are not available in Coq V7.0beta. |