Remove useless hypotheses for [path_sigT_uncurried_iff]

They were breaking tactics

1 files changed, 2 insertions, 2 deletions

diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v
index fc9d14d6f..f0016dc73 100644
--- a/src/Util/Sigma.v
+++ b/src/Util/Sigma.v
@@ -39,7 +39,7 @@ Section sigT.
     : u = v
     := path_sigT u v p (P_hprop _ _ _).
 
-  Definition path_sigT_uncurried_iff {A P} (P_hprop : forall (x : A) (p q : P x), p = q)
+  Definition path_sigT_uncurried_iff {A P}
              (u v : @sigT A P)
     : u = v <-> (sigT (fun p : projT1 u = projT1 v => eq_rect _ _ (projT2 u) _ p = projT2 v)).
   Proof.
@@ -101,7 +101,7 @@ Section sig.
     : u = v
     := path_sig u v p (P_hprop _ _ _).
 
-  Definition path_sig_uncurried_iff {A} {P : A -> Prop} (P_hprop : forall (x : A) (p q : P x), p = q)
+  Definition path_sig_uncurried_iff {A} {P : A -> Prop}
              (u v : @sig A P)
     : u = v <-> (sig (fun p : proj1_sig u = proj1_sig v => eq_rect _ _ (proj2_sig u) _ p = proj2_sig v)).
   Proof.