diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-03 15:14:17 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-03 15:14:17 -0400 |
| commit | 9009ddf4261bbf489874c4619a8c0397eb3f989d (patch) | |
| tree | b1fa7b5ff05300f1cca6f1eaf19b9fe3c601f6bf /src/Reflection/Z | |
| parent | eb20555b72dc38d4675cfb1e68203ad9be56a3d3 (diff) | |
Split off liftn_sig, add lift{3,4}_sig
Diffstat (limited to 'src/Reflection/Z')
| -rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/Glue.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/Bounds/Pipeline/Glue.v b/src/Reflection/Z/Bounds/Pipeline/Glue.v index af6a5548b..f3a0d8ee5 100644 --- a/src/Reflection/Z/Bounds/Pipeline/Glue.v +++ b/src/Reflection/Z/Bounds/Pipeline/Glue.v @@ -12,7 +12,7 @@ Require Import Crypto.Util.Curry. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.BoundedWord. Require Import Crypto.Util.Tuple. -Require Import Crypto.Util.SigmaAssoc. +Require Import Crypto.Util.Sigma.Associativity. Require Import Crypto.Util.Tactics.EvarExists. Module Export Exports. |