refactor `seq` permutation theory

- Change the naming of permutation lemmas so they conform to a
consistent policy: `perm_eq` lemmas have a `perm_` (_not_ `perm_eq`)
prefix, or sometimes a `_perm` suffix for lemmas that _prove_ `perm_eq`
using a property when there is also a lemma _using_ `perm_eq` for the
same property. Lemmas that do not concern `perm_eq` do _not_ have
`perm` in their name.
- Change the definition of `permutations` for a time- and space-
back-to-front generation algorithm.
- Add frequency tally operations `tally`, `incr_tally`, `wf_tally` and
`tally_seq`, used by the improved `permutation` algorithm.
- add deprecated aliases for renamed lemmas

1 files changed, 9 insertions, 0 deletions

diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 95da9cd..2925496 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -17,6 +17,15 @@ Global Set Bullet Behavior "None".
 (*    --> 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 _).  *)
+(*    --> Caveat 2: if premises or conclusions need to be adjusted, of for    *)
+(*        non-prenex implicits, use the idiom:                                *)
+(*         Notation old := ((fun a1 a2 ... => deprecate old new a1 a2 ...)    *)
+(*                          _ _ ... _) (only printing).                       *)
+(*        where all the implicit a_i's occur first, and correspond to the     *)
+(*        trailing _'s, making sure deprecate old new is fully applied and    *)
+(*        there are _no implicits_ inside the (fun .. => ..) expression. This *)
+(*        is to avoid triggering a bug in SSReflect elaboration that is       *)
+(*        triggered by such evars under binders.                              *)
 (*  Import Deprecation.Silent :: turn off deprecation warning messages.       *)
 (*  Import Deprecation.Reject :: raise an error instead of only warning.      *)
 (******************************************************************************)