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/PrimitiveSigma.v | |
| parent | 7ae0efa89026b0b0c19495bf2b085a90382ca4dd (diff) | |
Actually fix the build for Coq 8.7
Diffstat (limited to 'src/Util/PrimitiveSigma.v')
| -rw-r--r-- | src/Util/PrimitiveSigma.v | 1 |
1 files changed, 1 insertions, 0 deletions
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. |