aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorJason Gross2018-08-29 11:25:34 -0400
committerJason Gross2018-08-29 11:54:44 -0400
commit62bed22d2c104da07fc49b9c5f6229afedb92a07 (patch)
tree97053d3b85f8fc8a2b46c261870dd3f4e45d5cb5
parent06a00cf53442dacafd578b8db655e5d8097e9d84 (diff)
Move CHANGES entry for #8167 to 8.8.2 section
As per https://github.com/coq/coq/pull/8167#issuecomment-416929865
-rw-r--r--CHANGES15
1 files changed, 10 insertions, 5 deletions
diff --git a/CHANGES b/CHANGES
index 9bc2d2b369..a42c44c09b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -82,10 +82,6 @@ Tools
please open an issue. We can help set up external maintenance as part
of Proof-General, or independently as part of coq-community.
-- The targets `print-pretty-timed`, `print-pretty-timed-diff`, and
- `print-pretty-single-time-diff` now correctly label the "before" and
- "after" columns, rather than swapping them.
-
Vernacular Commands
@@ -158,7 +154,16 @@ Notations
Note that this might cause incompatibilities if you have, e.g., list_scope
and vector_scope both open with vector_scope on top, and expect `++` to
refer to `app`.
- Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want).
+ Solution: wrap `_ ++ _` in `(_ ++ _)%list` (or whichever scope you want).
+
+Changes from 8.8.1 to 8.8.2
+===========================
+
+Tools
+
+- The coq-makefile targets `print-pretty-timed`, `print-pretty-timed-diff`,
+ and `print-pretty-single-time-diff` now correctly label the "before" and
+ "after" columns, rather than swapping them.
Changes from 8.8.0 to 8.8.1
===========================