diff options
| author | herbelin | 2002-10-05 08:01:23 +0000 |
|---|---|---|
| committer | herbelin | 2002-10-05 08:01:23 +0000 |
| commit | c4db7eed5a1932a72466da2e31d86d362081f649 (patch) | |
| tree | 362bc1e488b4f0f5b4038d9c9694e0592feac7d5 | |
| parent | ade25271676f5e8dd4454ba8b3b3d7e3f8287633 (diff) | |
Le fichier CHANGES au format html - version 7.3.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8296 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/Changes.html | 126 |
1 files changed, 126 insertions, 0 deletions
diff --git a/doc/Changes.html b/doc/Changes.html new file mode 100644 index 0000000000..87082c6b8e --- /dev/null +++ b/doc/Changes.html @@ -0,0 +1,126 @@ +<HTML> +<body bgcolor=white> +<BR> +<b><font size=18>Changes from V7.3 to V7.3.1</font></b> +<BR> + +<H3>Bug fixes</H3> +<UL> +<LI> Corrupted Field tactic and Match Context tactic construction fixed +<LI> Checking of names already existing in Assert added (PR#182) +<LI> Invalid argument bug in Exact tactic solved (PR#183) +<LI> Colliding bound names bug fixed (PR#202) +<LI> Wrong non-recursivity test for Record fixed (PR#189) +<LI> Out of memory/seg fault bug related to parametric inductive fixed (PR#195) +<LI> Setoid_replace/Setoid_rewrite bug wrt "==" fixed +</UL> + +<H3>Miscellaneous</H3> +<UL> +<LI> Ocaml version >= 3.06 is needed to compile Coq from sources +<LI> Simplification of fresh names creation strategy for Assert, Pose and + LetTac (PR#192) +</UL> + +<BR> +<b><font size=18>Changes from V7.2 to V7.3</font></b> +<BR> + +<H3>Language</H3> +<UL> +<LI> Slightly improved compilation of pattern-matching (slight source of + incompatibilities) +<LI> Record's now accept anonymous fields "_" which does not build projections +<LI> Changes in the allowed elimination sorts for certain class of inductive + definitions : an inductive definition without constructors + of Sort Prop can be eliminated on sorts Set and Type A "singleton" + inductive definition (one constructor with arguments in the sort Prop + like conjunction of two propositions or equality) can be eliminated + directly on sort Type (In V7.2, only the sorts Prop and Set were allowed) +</UL> + +<H3>Tactics</H3> +<UL> +<LI> New tactic "Rename x into y" for renaming hypotheses +<LI> New tactics "Pose x:=u" and "Pose u" to add definitions to local context +<LI> Pattern now working on partially applied subterms +<LI> Ring no longer applies irreversible congruence laws of mult but + better applies congruence laws of plus (slight source of incompatibilities). +<LI> Intuition does no longer unfold constants except "<->" and "~". It + can be parameterized by a tactic. It also can introduce dependent + product if needed (source of incompatibilities) +<LI> "Match Context" now matching more recent hypotheses first and failing only + on user errors and Fail tactic (possible source of incompatibilities) +<LI> Tactic Definition's without arguments now allowed in Coq states +<LI> Better simplification and discrimination made by Inversion (source + of incompatibilities) +</UL> + +<H3>Bugs</H3> +<UL> +<LI> "Intros H" now working like "Intro H" trying first to reduce if not a product +<LI> Forward dependencies in Cases now taken into account +<LI> Known bugs related to Inversion and let-in's fixed +<LI> Bug unexpected Delta with let-in now fixed +</UL> + +<H3>Extraction (details in contrib/extraction/CHANGES or documentation)</H3> +<UL> +<LI> Signatures of extracted terms are now mostly expunged from dummy arguments. +<LI> Haskell extraction is now operational (tested & debugged). +</UL> + +<H3>Standard library</H3> +<UL> +<LI> Some additions in [ZArith]: three files (Zcomplements.v, Zpower.v + and Zlogarithms.v) moved from contrib/omega in order to be more + visible, one Zsgn function, more induction principles (Wf_Z.v and + tail of Zcomplements.v), one more general Euclid theorem +<LI> Peano_dec.v and Compare_dec.v now part of Arith.v +</UL> + +<H3>Tools</H3> +<UL> +<LI> new option -dump-glob to coqtop to dump globalizations (to be used by the + new documentation tool coqdoc; see http://www.lri.fr/~filliatr/coqdoc) +</UL> + +<H3>User Contributions</H3> +<UL> +<LI> CongruenceClosure (congruence closure decision procedure) +<LI> MapleMode (an interface to embed Maple simplification procedures in Coq) +<LI> Presburger (a formalization of Presburger's algorithm as stated in the initial paper by Presburger) +<LI> Chinese has been rewritten using Z from ZArith as datatype + ZChinese is the new version, Chinese the obsolete one +</UL> + +<H3>Incompatibilities</H3> +<UL> +<LI> Ring: exceptional incompatibilities (1 above 650 in submitted user + contribs, leading to a simplification) +<LI> Intuition: does not unfold any definition except "<->" and "~" +<LI> Cases: removal of some extra Cases in configurations of the form + "Cases ... of C _ => ... | _ D => ..." (effects on 2 definitions of + submitted user contributions necessitating the removal of now superfluous + proof steps in 3 different proofs) +<LI> Match Context, in case of incompatibilities because of a now non + trapped error (e.g. Not_found or Failure), use instead tactic Fail + to force Match Context trying the next clause +<LI> Inversion: better simplification and discrimination may occasionally + lead to less subgoals and/or hypotheses and different naming of hypotheses +<LI> Unification done by Apply/Elim has been changed and may exceptionally lead + to incompatible instantiations +<LI> Peano_dec.v and Compare_dec.v parts of Arith.v make Auto more + powerful if these files were not already required (1 occurrence of + this in submitted user contribs) +</UL> + +<BR><BR> +<HR> +<BR> + +<a href="ftp://ftp.inria.fr/INRIA/coq/V7.2/doc/Changes.html">Previous changes (from Coq V7.1 to V7.2)</a> +<BR> + +</BODY> +</HTML> |