Merge pull request #342 from math-comp/deprecation

add `deprecate` helper notation; no `perm` in non-`perm_eq` lemma names

1 files changed, 2 insertions, 0 deletions

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 ]"