diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-04 14:50:12 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-04 14:50:12 -0400 |
| commit | 6cba3c4e0572e9d917d3578c39f4f85cd3799b54 (patch) | |
| tree | 67cbdfff8e1f35c2898e0dc18f0848652e0dec04 /src/Specific | |
| parent | 7071632d516e361d6ad7dc10f5bbb7f39d4c4217 (diff) | |
Move sigma MapProjections to a separate file
Allows for more fine-grained imports
Diffstat (limited to 'src/Specific')
| -rw-r--r-- | src/Specific/IntegrationTest.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Specific/IntegrationTest.v b/src/Specific/IntegrationTest.v index 23b9f6579..6266d8dc7 100644 --- a/src/Specific/IntegrationTest.v +++ b/src/Specific/IntegrationTest.v @@ -7,7 +7,7 @@ Require Import Crypto.NewBaseSystem. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Specific.NewBaseSystemTest. Require Import Crypto.ModularArithmetic.PrimeFieldTheorems. -Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. +Require Import Crypto.Util.Tuple Crypto.Util.Sigma Crypto.Util.Sigma.MapProjections Crypto.Util.Sigma.Lift Crypto.Util.Notations Crypto.Util.ZRange Crypto.Util.BoundedWord. Require Import Crypto.Util.Tactics.Head. Import ListNotations. |