diff options
| author | affeldt-aist | 2020-11-20 12:41:11 +0900 |
|---|---|---|
| committer | GitHub | 2020-11-20 12:41:11 +0900 |
| commit | 3bb1ccc63170e3e71ef9d5b62758b6fdb1c4371c (patch) | |
| tree | 076b8d8c53eaaf424258388bbd0068970c55b85f /mathcomp/ssreflect/bigop.v | |
| parent | 676a9266ad77232ab198c86a6a3a3f3f6ba53cc0 (diff) | |
| parent | e565f8d9bebd4fd681c34086d5448dbaebc11976 (diff) | |
Merge pull request #658 from CohenCyril/duplicate_clear
Removing duplicate clears and turning the warning into an error
Diffstat (limited to 'mathcomp/ssreflect/bigop.v')
| -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 cd3507a..7d8332c 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1770,7 +1770,7 @@ rewrite -{P mem_r}big_r; elim: r Ur => /= [_ | i r IHr]. rewrite (big_pred1 [ffun=> j0]) ?big_nil //= => f. apply/familyP/eqP=> /= [Df |->{f} i]; last by rewrite ffunE !inE. by apply/ffunP=> i; rewrite ffunE; apply/eqP/Df. -case/andP=> /negbTE nri; rewrite big_cons big_distrl => {IHr}/IHr <-. +case/andP=> /negbTE nri; rewrite big_cons big_distrl => {}/IHr<-. rewrite (partition_big (fun f : fIJ => f i) (Q i)) => [|f]; last first. by move/familyP/(_ i); rewrite /= inE /= eqxx. pose seti j (f : fIJ) := [ffun k => if k == i then j else f k]. |