MAJ

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3668 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 167dd6528e..c1b126546e 100644
--- a/CHANGES
+++ b/CHANGES
@@ -109,6 +109,11 @@ Extraction (See details in contrib/extraction/CHANGES and README):
   thanks to automatic inserting of Obj.magic.
 - Experimental extraction of Coq new modules to Ocaml modules.
 
+Proof rendering in natural language
+
+- Export of theories to XML for publishing and rendering purposes now
+  includes proof-trees (see http://www.cs.unibo.it/helm)
+
 Miscellaneous
 
 - Printing Coercion now used through the standard keywords Set/Add, Test, Print