From c4db7eed5a1932a72466da2e31d86d362081f649 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 5 Oct 2002 08:01:23 +0000
Subject: 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
---
doc/Changes.html | 126 +++++++++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 126 insertions(+)
create mode 100644 doc/Changes.html
(limited to 'doc/Changes.html')
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 @@
+
+
+
+Changes from V7.3 to V7.3.1
+
+
+Bug fixes
+
+- Corrupted Field tactic and Match Context tactic construction fixed
+
- Checking of names already existing in Assert added (PR#182)
+
- Invalid argument bug in Exact tactic solved (PR#183)
+
- Colliding bound names bug fixed (PR#202)
+
- Wrong non-recursivity test for Record fixed (PR#189)
+
- Out of memory/seg fault bug related to parametric inductive fixed (PR#195)
+
- Setoid_replace/Setoid_rewrite bug wrt "==" fixed
+
+
+Miscellaneous
+
+- Ocaml version >= 3.06 is needed to compile Coq from sources
+
- Simplification of fresh names creation strategy for Assert, Pose and
+ LetTac (PR#192)
+
+
+
+Changes from V7.2 to V7.3
+
+
+Language
+
+- Slightly improved compilation of pattern-matching (slight source of
+ incompatibilities)
+
- Record's now accept anonymous fields "_" which does not build projections
+
- 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)
+
+
+Tactics
+
+- New tactic "Rename x into y" for renaming hypotheses
+
- New tactics "Pose x:=u" and "Pose u" to add definitions to local context
+
- Pattern now working on partially applied subterms
+
- Ring no longer applies irreversible congruence laws of mult but
+ better applies congruence laws of plus (slight source of incompatibilities).
+
- 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)
+
- "Match Context" now matching more recent hypotheses first and failing only
+ on user errors and Fail tactic (possible source of incompatibilities)
+
- Tactic Definition's without arguments now allowed in Coq states
+
- Better simplification and discrimination made by Inversion (source
+ of incompatibilities)
+
+
+Bugs
+
+- "Intros H" now working like "Intro H" trying first to reduce if not a product
+
- Forward dependencies in Cases now taken into account
+
- Known bugs related to Inversion and let-in's fixed
+
- Bug unexpected Delta with let-in now fixed
+
+
+Extraction (details in contrib/extraction/CHANGES or documentation)
+
+- Signatures of extracted terms are now mostly expunged from dummy arguments.
+
- Haskell extraction is now operational (tested & debugged).
+
+
+Standard library
+
+- 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
+
- Peano_dec.v and Compare_dec.v now part of Arith.v
+
+
+Tools
+
+- 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)
+
+
+User Contributions
+
+- CongruenceClosure (congruence closure decision procedure)
+
- MapleMode (an interface to embed Maple simplification procedures in Coq)
+
- Presburger (a formalization of Presburger's algorithm as stated in the initial paper by Presburger)
+
- Chinese has been rewritten using Z from ZArith as datatype
+ ZChinese is the new version, Chinese the obsolete one
+
+
+Incompatibilities
+
+- Ring: exceptional incompatibilities (1 above 650 in submitted user
+ contribs, leading to a simplification)
+
- Intuition: does not unfold any definition except "<->" and "~"
+
- 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)
+
- 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
+
- Inversion: better simplification and discrimination may occasionally
+ lead to less subgoals and/or hypotheses and different naming of hypotheses
+
- Unification done by Apply/Elim has been changed and may exceptionally lead
+ to incompatible instantiations
+
- 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)
+
+
+
+
+
+
+Previous changes (from Coq V7.1 to V7.2)
+
+
+
+
--
cgit v1.2.3