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 | |
parent | 7071632d516e361d6ad7dc10f5bbb7f39d4c4217 (diff) |
Move sigma MapProjections to a separate file
Allows for more fine-grained imports
Diffstat (limited to 'src')
-rw-r--r-- | src/Reflection/Z/Bounds/Pipeline/Definition.v | 2 | ||||
-rw-r--r-- | src/Specific/IntegrationTest.v | 2 | ||||
-rw-r--r-- | src/Util/Sigma.v | 5 | ||||
-rw-r--r-- | src/Util/Sigma/MapProjections.v | 6 |
4 files changed, 8 insertions, 7 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 *) 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. diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index 1c30219b7..222ebe89b 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -211,11 +211,6 @@ Section ex. Defined. End ex. -Definition projT2_map {A P Q} (f : forall a, P a -> Q a) (x : @sigT A P) : @sigT A Q - := let 'existT a p := x in existT Q a (f a p). -Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : @sig A P) : @sig A Q - := let 'exist a p := x in exist Q a (f a p). - (** ** Useful Tactics *) (** *** [inversion_sigma] *) (** The built-in [inversion] will frequently leave equalities of diff --git a/src/Util/Sigma/MapProjections.v b/src/Util/Sigma/MapProjections.v new file mode 100644 index 000000000..fd5556a33 --- /dev/null +++ b/src/Util/Sigma/MapProjections.v @@ -0,0 +1,6 @@ +Require Export Crypto.Util.GlobalSettings. + +Definition projT2_map {A P Q} (f : forall a, P a -> Q a) (x : @sigT A P) : @sigT A Q + := let 'existT a p := x in existT Q a (f a p). +Definition proj2_sig_map {A} {P Q : A -> Prop} (f : forall a, P a -> Q a) (x : @sig A P) : @sig A Q + := let 'exist a p := x in exist Q a (f a p). |