diff options
Diffstat (limited to 'src/Util')
| -rw-r--r-- | src/Util/Notations.v | 2 | ||||
| -rw-r--r-- | src/Util/PrimitiveSigma.v | 1 |
2 files changed, 3 insertions, 0 deletions
diff --git a/src/Util/Notations.v b/src/Util/Notations.v index 63ac9ac6a..455a02756 100644 --- a/src/Util/Notations.v +++ b/src/Util/Notations.v @@ -145,6 +145,8 @@ Reserved Notation "A ~> R" (at level 99). Reserved Notation "A --->" (left associativity, at level 65). Reserved Notation "'return' x" (at level 70, format "'return' x"). Reserved Notation "f x" (only printing, at level 10, left associativity). +(* TODO: Remove this next one if and when we drop support for Coq 8.7; it's present in the stdlib in 8.8 *) +Reserved Notation "{ x & P }" (at level 0, x at level 99). (* TODO: Uncomment this block when https://github.com/mit-plv/bbv/pull/13 is merged Reserved Notation "$ x" (at level 9, x at level 9, format "$ x"). Reserved Notation "# x" (at level 55, x at level 9, format "# x"). (* 55, so we don't clash with [_ # _] *) diff --git a/src/Util/PrimitiveSigma.v b/src/Util/PrimitiveSigma.v index a3b124821..5a182e544 100644 --- a/src/Util/PrimitiveSigma.v +++ b/src/Util/PrimitiveSigma.v @@ -9,6 +9,7 @@ Require Import Coq.Classes.Morphisms. Require Import Crypto.Util.IffT. Require Import Crypto.Util.Equality. Require Import Crypto.Util.GlobalSettings. +Require Import Crypto.Util.Notations. Local Set Primitive Projections. |