diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-03 15:45:01 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-10-03 15:45:01 +0000 |
| commit | b0b98c1a236fca450a183ecae5157ed70e3da6c6 (patch) | |
| tree | 3f3bf0db26d008a9c5df03d79fa936db16e33f3a /CHANGES | |
| parent | 84566056d2f020347d781b10f97d77155ed45a95 (diff) | |
Intégration des modifs de la V7.3.1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3086 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 20 |
1 files changed, 19 insertions, 1 deletions
@@ -1,4 +1,4 @@ -Changes from V7.3 to ???? +Changes from V7.3.1 to ???? ------------------------- Library @@ -61,6 +61,24 @@ Incompatibilities proofs; in some cases, incompatibilites is solved by declaring locally opaque the relevant constant) +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 + +Misc + + - 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 ------------------------- |