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.

8 files changed, 113 insertions, 15 deletions

diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 3eae6fa..65a71ed 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -159,9 +159,14 @@ ci-fourcolor-dev:
     - make install
 
 ci-odd-order-8.7:
-  extends: .ci-odd-order
-  variables:
-    COQ_VERSION: "8.7"
+ extends: .ci-odd-order
+ variables:
+   COQ_VERSION: "8.7"
+
+ci-odd-order-8.8:
+ extends: .ci-odd-order
+ variables:
+   COQ_VERSION: "8.8"
 
 ci-odd-order-dev:
   extends: .ci-odd-order
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
 
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 468aa66..65167b5 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -2412,7 +2412,7 @@ Proof.
 set Su := map _ S => sSuS freeS; have uniqS := free_uniq freeS.
 have uniqSu: uniq Su by rewrite (map_inj_uniq cfAut_inj).
 have{sSuS} sSuS: {subset Su <= S} by move=> _ /mapP[phi Sphi ->]; apply: sSuS.
-have [|eqSuS _] := leq_size_perm uniqSu sSuS; first by rewrite size_map.
+have [|_ eqSuS] := uniq_min_size uniqSu sSuS; first by rewrite size_map.
 by rewrite (perm_free (uniq_perm_eq uniqSu uniqS eqSuS)).
 Qed.
 
diff --git a/mathcomp/field/galois.v b/mathcomp/field/galois.v
index 459250f..ae54fa1 100644
--- a/mathcomp/field/galois.v
+++ b/mathcomp/field/galois.v
@@ -1332,9 +1332,9 @@ rewrite -coef_map rmorph_prod; congr (_ : {poly _})`_i.
 symmetry; rewrite (eq_big_perm (map x r)) /= ?(big_map x).
   by apply: eq_bigr => b _; rewrite rmorphB /= map_polyX map_polyC.
 have Uxr: uniq (map x r) by rewrite map_inj_uniq //; apply: fmorph_inj.
-have /leq_size_perm: {subset map x r <= r}.
+have /uniq_min_size: {subset map x r <= r}.
   by rewrite -map_comp => _ /codomP[b ->] /=; rewrite -galM // r_xa ?groupM.
-by rewrite (size_map x) perm_eq_sym; case=> // /uniq_perm_eq->.
+by rewrite (size_map x) perm_eq_sym; case=> // _ /uniq_perm_eq->.
 Qed.
 
 Lemma mem_galTrace K E a : galois K E -> a \in E -> galTrace K E a \in K.
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index 5576355..3685c23 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1516,26 +1516,26 @@ move=> Us1 eqs12; apply/idP/idP=> [Us2 | /eqP eq_sz12].
 by apply: (leq_size_uniq Us1) => [y|]; rewrite (eqs12, eq_sz12).
 Qed.
 
-Lemma leq_size_perm s1 s2 :
+Lemma uniq_min_size s1 s2 :
     uniq s1 -> {subset s1 <= s2} -> size s2 <= size s1 ->
-  s1 =i s2 /\ size s1 = size s2.
+  (size s1 = size s2) * (s1 =i s2).
 Proof.
 move=> Us1 ss12 le_s21; have Us2: uniq s2 := leq_size_uniq Us1 ss12 le_s21.
-suffices: s1 =i s2 by split; last by apply/eqP; rewrite -uniq_size_uniq.
+suffices: s1 =i s2 by split; first by apply/eqP; rewrite -uniq_size_uniq.
 move=> x; apply/idP/idP=> [/ss12// | s2x]; apply: contraLR le_s21 => not_s1x.
 rewrite -ltnNge (@uniq_leq_size (x :: s1)) /= ?not_s1x //.
 by apply/allP; rewrite /= s2x; apply/allP.
 Qed.
 
-Lemma perm_uniq s1 s2 : s1 =i s2 -> size s1 = size s2 -> uniq s1 = uniq s2.
+Lemma eq_uniq s1 s2 : size s1 = size s2 -> s1 =i s2 -> uniq s1 = uniq s2.
 Proof.
-move=> Es12 Esz12.
-by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?Esz12 ?eqxx.
+move=> eq_sz12 eq_s12.
+by apply/idP/idP=> Us; rewrite (uniq_size_uniq Us) ?eq_sz12 ?eqxx.
 Qed.
 
 Lemma perm_eq_uniq s1 s2 : perm_eq s1 s2 -> uniq s1 = uniq s2.
 Proof.
-by move=> eq_s12; apply: perm_uniq; [apply: perm_eq_mem | apply: perm_eq_size].
+by move=> eq_s12; apply/eq_uniq; [apply: perm_eq_size | apply: perm_eq_mem].
 Qed.
 
 Lemma uniq_perm_eq s1 s2 : uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq s1 s2.
@@ -3056,3 +3056,16 @@ Coercion all_iffP : all_iff >-> Funclass.
 Notation "[ '<->' P0 ; P1 ; .. ; Pn ]" := (all_iff P0 (P1 :: .. [:: Pn] ..))
   (at level 0, format "[ '<->' '['  P0 ;  '/' P1 ;  '/'  .. ;  '/'  Pn ']' ]")
   : form_scope.
+
+Notation leq_size_perm :=
+  ((fun T s1 s2 Us1 ss12 les21 =>
+   let: (Esz12, Es12) :=
+     deprecate leq_size_perm uniq_min_size T s1 s2 Us1 ss12 les21
+   in conj Es12 Esz12) _ _ _)
+  (only parsing).
+Notation perm_uniq :=
+  ((fun T s1 s2 eq_s12 eq_sz12 =>
+      deprecate perm_uniq eq_uniq T s1 s2 eq_sz12 eq_s12)
+    _ _ _)
+  (only parsing).
+
diff --git a/mathcomp/ssreflect/ssrbool.v b/mathcomp/ssreflect/ssrbool.v
index 7eb7fd9..54c74dd 100644
--- a/mathcomp/ssreflect/ssrbool.v
+++ b/mathcomp/ssreflect/ssrbool.v
@@ -1,6 +1,18 @@
 From mathcomp Require Import ssreflect ssrfun.
 From Coq Require Export ssrbool.
 
+(******************************************************************************)
+(* Local additions:                                                           *)
+(*      {pred T} == a type convertible to pred T but that presents the        *)
+(*                  pred_sort coercion class.                                 *)
+(*  PredType toP == the predType structure for toP : A -> pred T.             *)
+(*    relpre f r == the preimage of r by f, simplifying to r (f x) (f y).     *)
+(* --> These will become part of the core SSReflect library with Coq 8.11.    *)
+(* This file also anticipates a v8.11 change in the definition of simpl_pred  *)
+(* to T -> simpl_pred T. This change ensures that inE expands the definition  *)
+(* of r : simpl_rel along with the \in, when rewriting in y \in r x.          *)
+(******************************************************************************)
+
 Notation "{ 'pred' T }" := (pred_sort (predPredType T)) (at level 0,
   format "{ 'pred'  T }") : type_scope.
 
@@ -37,4 +49,3 @@ Notation "[ 'rel' x y 'in' A ]" := [rel x y in A & A] (at level 0,
 Notation xrelpre := (fun f (r : rel _) x y => r (f x) (f y)).
 Definition relpre {T rT} (f : T -> rT)  (r : rel rT) :=
   [rel x y | r (f x) (f y)].
-
diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index fe06c0d..95da9cd 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -5,6 +5,22 @@ Global Set SsrOldRewriteGoalsOrder.
 Global Set Asymmetric Patterns.
 Global Set Bullet Behavior "None".
 
+(******************************************************************************)
+(* Local additions:                                                           *)
+(*   nonPropType == an interface for non-Prop Types: a nonPropType coerces    *)
+(*                  to a Type, and only types that do _not_ have sort         *)
+(*                  Prop are canonical nonPropType instances. This is         *)
+(*                  useful for applied views.                                 *)
+(*   --> This will become standard with the Coq v8.11 SSReflect core library. *)
+(*  deprecate old new == new, but warning that old is deprecated and new      *)
+(*                       should be used instead.                              *)
+(*    --> Usage: Notation old := (deprecate old new) (only parsing).          *)
+(*    --> Caveat: deprecate old new only inherits new's maximal implicits;    *)
+(*        on-demand implicits should be added after : (deprecate old new _).  *)
+(*  Import Deprecation.Silent :: turn off deprecation warning messages.       *)
+(*  Import Deprecation.Reject :: raise an error instead of only warning.      *)
+(******************************************************************************)
+
 Module NonPropType.
 
 Structure call_of (condition : unit) (result : bool) := Call {callee : Type}.
@@ -33,3 +49,39 @@ End Exports.
 End NonPropType.
 Export NonPropType.Exports.
 
+Module Deprecation.
+
+Definition hidden (T : Type) := T.
+Definition exposed (T : Type) & unit -> unit -> unit := T.
+Definition hide T u (v : exposed T u) : hidden T := v.
+
+Ltac warn old_id new_id :=
+  idtac "Warning:" old_id "is deprecated; use" new_id "instead".
+
+Ltac stop old_id new_id :=
+  fail 1 "Error:" old_id "is deprecated; use" new_id "instead".
+
+Structure hinted := Hint {statement; hint : statement}.
+Ltac check cond := let test := constr:(hint _ : cond) in idtac.
+
+Variant reject := Reject.
+Definition reject_hint := Hint reject Reject.
+Module Reject. Canonical reject_hint. End Reject.
+
+Variant silent := Silent.
+Definition silent_hint := Hint silent Silent.
+Module Silent. Canonical silent_hint. End Silent.
+
+Ltac flag old_id new_id :=
+  first [check reject; stop old_id new_id | check silent | warn old_id new_id].
+
+Module Exports.
+Arguments hide {T} u v /.
+Coercion hide : exposed >-> hidden.
+Notation deprecate old_id new_id :=
+  (hide (fun old_id new_id => ltac:(flag old_id new_id; exact tt)) new_id)
+  (only parsing).
+End Exports.
+
+End Deprecation.
+Export Deprecation.Exports.
diff --git a/mathcomp/ssreflect/ssrnotations.v b/mathcomp/ssreflect/ssrnotations.v
index 4c55514..dbc7f3d 100644
--- a/mathcomp/ssreflect/ssrnotations.v
+++ b/mathcomp/ssreflect/ssrnotations.v
@@ -1,6 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 
+(******************************************************************************)
 (* - Reserved notation for various arithmetic and algebraic operations:       *)
 (*     e.[a1, ..., a_n] evaluation (e.g., polynomials).                       *)
 (*                 e`_i indexing (number list, integer pi-part).              *)
@@ -27,6 +28,7 @@
 (*    [rec a1, ..., an] standard shorthand for hidden recursor (see prime.v). *)
 (*   The interpretation of these notations is not defined here, but the       *)
 (*   declarations help maintain consistency across the library.               *)
+(******************************************************************************)
 
 (* Reserved notation for evaluation *)
 Reserved Notation "e .[ x ]"