From b59653a5b377f91a21e8036bf0b5d98a35fc4963 Mon Sep 17 00:00:00 2001
From: Georges Gonthier
Date: Sun, 5 May 2019 17:01:50 +0200
Subject: add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma
 names

- add notation support for lemma renaming PRs, helping clients adjust
to the name change by emitting warning or raising errors when the old
name is used. The default is to emit warnings, but clients can change
this to silence (if electing to delay migration) or errors (to help
with actual migration). Usage:
  Notation old_id := (deprecate old_id new_id) (only parsing).
—> Caveat 1: only prenex maximal implicit of `new_id` are preserved, so,
as `Notation` does not support on-demand implicits, the latter should
be added explicitly as in `(deprecate old new _ _)`.
—> Caveat 2: the warnings are emitted by a tactic-in-term, which
is interpreted during type elaboration. As the SSReflect elaborator may
re-infer type in arguments multiple times (notably, views and arguments
to `apply` and `rewrite`), clients may see duplicate warnings.
- use the `deprecate` facility to introduce the first part of the
refactoring of `seq` permutation lemmas : only lemmas concerning
`perm_eq` should have `perm` as a component of their name.
- document local additions in `ssreflect.v` and `ssrbool.v`
- add 8.8 `odd-order` regression
- the explicit beta-redex idiom use in the `perm_uniq` and
`leq_min_perm` aliases avoids a strange name-sensitive bug of view
interpretation in Coq 8.7.
---
 CHANGELOG.md | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'CHANGELOG.md')

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 99f51ce..3361567 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -9,10 +9,24 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 
 ### Added
 
+- `nonPropType`, an interface for non-`Prop` types, and `{pred T}` and
+   `relpre f r`, all of which will be in the Coq 8.11 core SSreflect library.
+
+- `deprecate old_id new_id`, notation for `new_id` that prints a deprecation
+  warning for `old_id`; `Import Deprecation.Silent` turns off those warnings,
+  `Import Deprecation.Reject` raises errors instead of only warning.
+
 ### Changed
 
+- definition of `PredType` which now takes only a `P -> pred T` function;
+  definition of `simpl_rel` to improve simplification by `inE`. Both these
+  changes will be in the Coq 8.11 SSReflect core library.
+
 ### Renamed
 
+- `leq_size_perm` -> `uniq_min_size` (permuting conclusions)
+- `perm_uniq` -> `eq_uniq` (permuting assumptions)
+
 ### Misc
 
 ## [1.8.0] - 2019-04-08
@@ -58,7 +72,8 @@ MathComp 1.8.0 is compatible with Coq 8.7, 8.8 and 8.9.
 
 - a function `permutations` that computes a duplicate-free list
   of all permutations of a given sequence `s` over an `eqType`, along
-  whit its theory.
+  with its theory: `mem_permutations`, `size_permutations`,
+  `permutations_uniq`, `permutations_all_uniq`, `perm_permutations`.
 
 ### Changed
 
-- 
cgit v1.2.3