update CHANGES

.gitignore

@@ -206,4 +206,4 @@ pvsbin/
 /src/jessie/config.status
 /src/jessie/Makefile
 /src/jessie/ptests_local_config.ml
-/src/jessie/tests/basic/result/*.log
\ No newline at end of file
+/src/jessie/tests/basic/result/*.log

CHANGES

@@ -2,11 +2,28 @@
 
 version 0.80, Oct 30, 2012
 ==========================
-  o new warning: form exists x, P -> Q
-  o [replayer] new option -q
+  * Modified syntax for mlw programs. A summary of changes is given in
+    the manual, in Appendix A
+  o Programs support type invariants and ghost code
+  o Ocaml modules for constructing program modules are included in the
+    Why3 library and API
+  o New transformations for induction of integers or on algebraic
+    types
+  o New system of warnings, that includes:
+     - form "exists x, P -> Q", likely an error
+     - unused bound logic variables in "forall", "exists" and "let"
+  o [replayer] new option -q, for running quietly
   o [Provers] support for Coq 8.4
-  o new scheme for Coq realizations, using type classes
-  * theory realizations now use meta "realized_theory" instead of "realized"
+  * [Provers] dropped support for Coq 8.2
+  o [Provers] Support for PVS 6.0, including realizations
+  o [Provers] support for iProver and Zenon
+  * improved output of "why3session latex", LaTeX macros have more
+    arguments
+  o New scheme for Coq realizations, using type classes
+  * theory realizations now use meta "realized_theory" instead of
+    "realized"
+  * sections in --extra-config are called [prover_modifier] instead of
+    [prover]
 
 version 0.73, Jul 19, 2012
 ==========================

Makefile.in

@@ -1441,6 +1441,7 @@ $(DISTRIB_TAR): doc/manual.pdf
 	ln -s ../modules $(DISTRIB_DIR)/share/modules
 	ln -s ../theories $(DISTRIB_DIR)/share/theories
 	cp --parents $(DISTRIB_FILES) $(DISTRIB_DIR)
+	rm -rf $(DISTRIB_DIR)/examples/hoare_logic
 	cd $(DISTRIB_DIR); rm -f $(LIBGENERATED) \
           $(COQPGENERATED) $(WHY3DOCGENERATED) $(PLUGGENERATED)
 	cd distrib; tar cf $(NAME).tar $(NAME); gzip -f --best $(NAME).tar

examples/programs/hamming_sequence/why3session.xml

+<?xml version="1.0" encoding="UTF-8"?>
+<!DOCTYPE why3session SYSTEM "/home/cmarche/recherche/why3/share/why3session.dtd">
+<why3session shape_version="2">
+ <file
+  name="../hamming_sequence.mlw"
+  verified="false"
+  expanded="true">
+  <theory
+   name="HammingSequence"
+   locfile="../hamming_sequence.mlw"
+   loclnum="13" loccnumb="7" loccnume="22"
+   verified="false"
+   expanded="true">
+   <goal
+    name="WP_parameter hamming"
+    locfile="../hamming_sequence.mlw"
+    loclnum="23" loccnumb="6" loccnume="13"
+    expl="VC for hamming"
+    sum="f44ece18b0be5dcc595e579828a6c5bf"
+    proved="false"
+    expanded="true"
+    shape="ainfix =agetV7V8ahammingV8Iainfix &lt;V8V0Aainfix &lt;=c0V8FIainfix &gt;V2agetV7ainfix +ainfix -V0c1c1Aainfix &gt;V4agetV7ainfix +ainfix -V0c1c1Aainfix &gt;V6agetV7ainfix +ainfix -V0c1c1Aainfix =V2ainfix *c5agetV7V1Aainfix =V4ainfix *c3agetV7V3Aainfix =V6ainfix *c2agetV7V5Aiainfix &lt;=V12aminV6aminV4V2ainfix &lt;V13V0Aainfix &lt;=c0V13Iainfix =V13ainfix +V11c1Fiainfix &lt;=V15aminV6aminV4V2ainfix &lt;V16V0Aainfix &lt;=c0V16Iainfix =V16ainfix +V14c1Fiainfix &lt;=V18aminV6aminV4V2ainfix &lt;V19V0Aainfix &lt;=c0V19Iainfix =V19ainfix +V17c1Fainfix &gt;V18agetV10ainfix +V9c1Aainfix &gt;V15agetV10ainfix +V9c1Aainfix &gt;V12agetV10ainfix +V9c1Aainfix =V18ainfix *c5agetV10V17Aainfix =V15ainfix *c3agetV10V14Aainfix =V12ainfix *c2agetV10V11FFFIainfix =V10asetV7V9aminV6aminV4V2FAainfix &lt;V9V0Aainfix &lt;=c0V9Iainfix &gt;V2agetV7V9Aainfix &gt;V4agetV7V9Aainfix &gt;V6agetV7V9Aainfix =V2ainfix *c5agetV7V1Aainfix =V4ainfix *c3agetV7V3Aainfix =V6ainfix *c2agetV7V5Iainfix &lt;=V9ainfix -V0c1Aainfix &lt;=c0V9FFAainfix &gt;c5agetaconstc0c0Aainfix &gt;c3agetaconstc0c0Aainfix &gt;c2agetaconstc0c0Aainfix =c5ainfix *c5agetaconstc0c0Aainfix =c3ainfix *c3agetaconstc0c0Aainfix =c2ainfix *c2agetaconstc0c0Iainfix &lt;=c0ainfix -V0c1Aainfix =agetaconstc0V20ahammingV20Iainfix &lt;V20V0Aainfix &lt;=c0V20FIainfix &gt;c0ainfix -V0c1Aainfix &gt;=V0c0Iainfix &gt;=V0c1F">
+    <label
+     name="expl:VC for hamming"/>
+   </goal>
+  </theory>
+ </file>
+</why3session>