diff options
| author | Cyril Cohen | 2020-09-01 14:28:29 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-01 14:28:29 +0200 |
| commit | 58efec880eeae2e3046eb798fe4b38d9572990c2 (patch) | |
| tree | 5b37078fb4012274d3c20e7c696c37234758c0df | |
| parent | 2d9c3d1775917a4e89d012efaf40539d9b0b72bd (diff) | |
fix for Coq 8.7
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index af1bcec..1b580c0 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1539,7 +1539,7 @@ Qed. Lemma sig_big_dep (I : finType) (J : I -> finType) (P : pred I) (Q : forall {i}, pred (J i)) (F : forall {i}, J i -> R) : \big[op/idx]_(i | P i) \big[op/idx]_(j : J i | Q j) F j = - \big[op/idx]_(p : {i & J i} | P (tag p) && Q (tagged p)) F (tagged p). + \big[op/idx]_(p : {i : I & J i} | P (tag p) && Q (tagged p)) F (tagged p). Proof. pose s := [seq Tagged J j | i <- index_enum I, j <- index_enum (J i)]. rewrite [LHS]big_mkcond big_mkcondl [RHS]big_mkcond -[RHS](@perm_big _ s). |