diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-09-16 18:29:07 -0400 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2018-09-17 00:25:44 -0400 |
| commit | 7c41e71c4c3f292c33ff10b869e91f98091f4ca6 (patch) | |
| tree | c2fd502a5a30c6902102512cfdeff566d849eb7c /src/Util | |
| parent | 7ae0efa89026b0b0c19495bf2b085a90382ca4dd (diff) | |
Actually fix the build for Coq 8.7
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. |