diff options
Diffstat (limited to 'mathcomp/ssreflect/ssrnotations.v')
| -rw-r--r-- | mathcomp/ssreflect/ssrnotations.v | 2 |
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 ]" |