From 6cf8d80ac0a9869d97373d6813441eabebce8980 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 23 Feb 2006 13:58:10 +0000
Subject: Nettoyage de l'archive doc et restructuration avant intégration à
l'archive principale de Coq et publication des sources (HH)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8606 85f007b7-540e-0410-9357-904b9bb8a0f7
---
doc/Changes.html | 126 -------------------------------------------------------
1 file changed, 126 deletions(-)
delete mode 100644 doc/Changes.html
(limited to 'doc/Changes.html')
diff --git a/doc/Changes.html b/doc/Changes.html
deleted file mode 100644
index 87082c6b8e..0000000000
--- a/doc/Changes.html
+++ /dev/null
@@ -1,126 +0,0 @@
-
-
-
-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