aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-04 20:59:28 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-04 20:59:28 +0200
commitb0ed0c2c1c7ca8fc434ecadd3a9ed906e6e428c2 (patch)
tree877b7cf28198b4441282cb860646aed99124fdae /CHANGES
parentd8f85f473a41037544c41d62c0ed1b70430abd14 (diff)
parent2a628bbdd86f501b24074343653fdafa6e14c94a (diff)
Merge PR #7486: Update old parts of CHANGES to use current bug numbers.
Diffstat (limited to 'CHANGES')
-rw-r--r--CHANGES44
1 files changed, 22 insertions, 22 deletions
diff --git a/CHANGES b/CHANGES
index a5a5afcbf..5b5885487 100644
--- a/CHANGES
+++ b/CHANGES
@@ -125,7 +125,7 @@ Tactics
profiling, and "Set NativeCompute Profile Filename" customizes
the profile filename.
- The tactic "omega" is now aware of the bodies of context variables
- such as "x := 5 : Z" (see BZ#148). This could be disabled via
+ such as "x := 5 : Z" (see #1362). This could be disabled via
Unset Omega UseLocalDefs.
- The tactic "romega" is also aware now of the bodies of context variables.
- The tactic "zify" resp. "omega with N" is now aware of N.pred.
@@ -310,7 +310,7 @@ Improvements around some error messages.
Many bug fixes including two important ones:
-- BZ#5730: CoqIDE becomes unresponsive on file open.
+- Bug #5730: CoqIDE becomes unresponsive on file open.
- coq_makefile: make sure compile flags for Coq and coq_makefile are in sync
(in particular, make sure the `-safe-string` option is used to compile plugins).
@@ -360,7 +360,7 @@ Tactics
which behave like the corresponding variants with no "e" but turn
unresolved implicit arguments into existential variables, on the
shelf, rather than failing.
-- Tactic injection has become more powerful (closes BZ#4890) and its
+- Tactic injection has become more powerful (closes bug #4890) and its
documentation has been updated.
- New variants of the `first` and `solve` tacticals that do not rely
on parsing rules, meant to define tactic notations.
@@ -406,7 +406,7 @@ Standard Library
file ChoiceFacts.v.
- New lemmas about iff and about orders on positive and Z.
- New lemmas on powerRZ.
-- Strengthened statement of JMeq_eq_dep (closes BZ#4912).
+- Strengthened statement of JMeq_eq_dep (closes bug #4912).
- The BigN, BigZ, BigZ libraries are no longer part of the Coq standard
library, they are now provided by a separate repository
https://github.com/coq/bignums
@@ -481,12 +481,12 @@ XML Protocol and internal changes
See dev/doc/changes.txt
-Many bugfixes including BZ#1859, BZ#2884, BZ#3613, BZ#3943, BZ#3994,
-BZ#4250, BZ#4709, BZ#4720, BZ#4824, BZ#4844, BZ#4911, BZ#5026, BZ#5233,
-BZ#5275, BZ#5315, BZ#5336, BZ#5360, BZ#5390, BZ#5414, BZ#5417, BZ#5420,
-BZ#5439, BZ#5449, BZ#5475, BZ#5476, BZ#5482, BZ#5501, BZ#5507, BZ#5520,
-BZ#5523, BZ#5524, BZ#5553, BZ#5577, BZ#5578, BZ#5589, BZ#5597, BZ#5598,
-BZ#5607, BZ#5618, BZ#5619, BZ#5620, BZ#5641, BZ#5648, BZ#5651, BZ#5671.
+Many bugfixes including #1859, #2884, #3613, #3943, #3994,
+#4250, #4709, #4720, #4824, #4844, #4911, #5026, #5233,
+#5275, #5315, #5336, #5360, #5390, #5414, #5417, #5420,
+#5439, #5449, #5475, #5476, #5482, #5501, #5507, #5520,
+#5523, #5524, #5553, #5577, #5578, #5589, #5597, #5598,
+#5607, #5618, #5619, #5620, #5641, #5648, #5651, #5671.
Many bugfixes on OS X and Windows (now the test-suite passes on these
platforms too).
@@ -2662,7 +2662,7 @@ Tactics
a registered setoid equality before starting to reduce in H. This is unlikely
to break any script. Should this happen nonetheless, one can insert manually
some "unfold ... in H" before rewriting.
-- Fixed various bugs about (setoid) rewrite ... in ... (in particular BZ#1101)
+- Fixed various bugs about (setoid) rewrite ... in ... (in particular bug #5941)
- "rewrite ... in" now accepts a clause as place where to rewrite instead of
juste a simple hypothesis name. For instance:
rewrite H in H1,H2 |- * means rewrite H in H1; rewrite H in H2; rewrite H
@@ -3239,11 +3239,11 @@ Incompatibilities
Bugs
- Improved localisation of errors in Syntactic Definitions
-- Induction principle creation failure in presence of let-in fixed (BZ#238)
-- Inversion bugs fixed (BZ#212 and BZ#220)
-- Omega bug related to Set fixed (BZ#180)
-- Type-checking inefficiency of nested destructuring let-in fixed (BZ#216)
-- Improved handling of let-in during holes resolution phase (BZ#239)
+- Induction principle creation failure in presence of let-in fixed (#1459)
+- Inversion bugs fixed (#1427 and #1437)
+- Omega bug related to Set fixed (#1384)
+- Type-checking inefficiency of nested destructuring let-in fixed (#1435)
+- Improved handling of let-in during holes resolution phase (#1460)
Efficiency
@@ -3256,18 +3256,18 @@ 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 (BZ#182)
- - Invalid argument bug in Exact tactic solved (BZ#183)
- - Colliding bound names bug fixed (BZ#202)
- - Wrong non-recursivity test for Record fixed (BZ#189)
- - Out of memory/seg fault bug related to parametric inductive fixed (BZ#195)
+ - Checking of names already existing in Assert added (#1386)
+ - Invalid argument bug in Exact tactic solved (#1387)
+ - Colliding bound names bug fixed (#1412)
+ - Wrong non-recursivity test for Record fixed (#1394)
+ - Out of memory/seg fault bug related to parametric inductive fixed (#1404)
- 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 (BZ#192)
+ LetTac (#1402)
Changes from V7.2 to V7.3
=========================