diff options
Diffstat (limited to 'src/Util/Sigma.v')
| -rw-r--r-- | src/Util/Sigma.v | 5 |
1 files changed, 0 insertions, 5 deletions
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 |