Move sigma MapProjections to a separate file

Allows for more fine-grained imports

5 files changed, 9 insertions, 7 deletions

diff --git a/_CoqProject b/_CoqProject
index 942930051..09eafa01e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -285,6 +285,7 @@ src/Util/ZRange.v
 src/Util/ZUtil.v
 src/Util/Sigma/Associativity.v
 src/Util/Sigma/Lift.v
+src/Util/Sigma/MapProjections.v
 src/Util/Tactics/BreakMatch.v
 src/Util/Tactics/ClearDuplicates.v
 src/Util/Tactics/Contains.v
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).