From 9c8f15339e719321d1a04360d3d2052ecd8bb5a2 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Wed, 20 Mar 2019 18:31:45 +0100
Subject: Compat of sumn with bigop and renaming dep to cond when appropriate

---
 mathcomp/ssreflect/binomial.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/ssreflect/binomial.v')

diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index 98ee64e..1f0ae16 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -387,7 +387,7 @@ have [ltTk | lekT] := ltnP #|B| k.
   have [AsubB /=|//] := boolP (A \subset B).
   by rewrite (leq_ltn_trans (subset_leq_card AsubB)) ?andbF.
 apply/eqP; rewrite -(eqn_pmul2r (fact_gt0 k)) bin_ffact // eq_sym.
-rewrite -sum_nat_dep_const -{1 3}(card_ord k).
+rewrite -sum_nat_cond_const -{1 3}(card_ord k).
 rewrite -card_inj_ffuns_on -sum1dep_card.
 pose imIk (f : {ffun 'I_k -> T}) := f @: 'I_k.
 rewrite (partition_big imIk (fun A => (A \subset B) && (#|A| == k))) /=
-- 
cgit v1.2.3