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.

1 files changed, 52 insertions, 0 deletions

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.