diff options
author | 2017-04-04 14:50:12 -0400 | |
---|---|---|
committer | 2017-04-04 14:50:12 -0400 | |
commit | 6cba3c4e0572e9d917d3578c39f4f85cd3799b54 (patch) | |
tree | 67cbdfff8e1f35c2898e0dc18f0848652e0dec04 /src/Reflection/Z | |
parent | 7071632d516e361d6ad7dc10f5bbb7f39d4c4217 (diff) |
Move sigma MapProjections to a separate file
Allows for more fine-grained imports
Diffstat (limited to 'src/Reflection/Z')
-rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/Definition.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/Bounds/Pipeline/Definition.v b/src/Reflection/Z/Bounds/Pipeline/Definition.v index 1c2508bd7..98d3078c3 100644 --- a/src/Reflection/Z/Bounds/Pipeline/Definition.v +++ b/src/Reflection/Z/Bounds/Pipeline/Definition.v @@ -62,7 +62,7 @@ Require Import Crypto.Reflection.LinearizeWf. Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijn. Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijnInterp. Require Import Crypto.Reflection.Z.Bounds.MapCastByDeBruijnWf. -Require Import Crypto.Util.Sigma. +Require Import Crypto.Util.Sigma.MapProjections. (** *** Definition of the Post-Wf Pipeline *) (** Do not change the name or the type of this definition *) |