diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-01-19 14:05:54 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-01-19 14:05:54 -0500 |
| commit | cded6731f79a66018d3660017bda7a284aedf50c (patch) | |
| tree | 1311ed7d6d0bf9a06a5ad86531a708de4e95e19d /src/Reflection/Z/Syntax.v | |
| parent | cb98e6d8a45b68e29546732a0eed969c724a0274 (diff) | |
Split out Reflection.Equality, change Tflat implicit argument
Diffstat (limited to 'src/Reflection/Z/Syntax.v')
| -rw-r--r-- | src/Reflection/Z/Syntax.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Reflection/Z/Syntax.v b/src/Reflection/Z/Syntax.v index 466dbd4b5..ea867d024 100644 --- a/src/Reflection/Z/Syntax.v +++ b/src/Reflection/Z/Syntax.v @@ -1,6 +1,7 @@ (** * PHOAS Syntax for expression trees on ℤ *) Require Import Coq.ZArith.ZArith. Require Import Crypto.Reflection.Syntax. +Require Import Crypto.Reflection.Equality. Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations. Require Import Crypto.Util.Equality. Require Import Crypto.Util.ZUtil. |