From 7c41e71c4c3f292c33ff10b869e91f98091f4ca6 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 16 Sep 2018 18:29:07 -0400 Subject: Actually fix the build for Coq 8.7 --- src/Util/Notations.v | 2 ++ src/Util/PrimitiveSigma.v | 1 + 2 files changed, 3 insertions(+) (limited to 'src/Util') 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. -- cgit v1.2.3