coq-mathcomp/mathcomp, branch master Library of mathematical components formalized in Coq Update mathcomp/ssreflect/path.v 2021-03-23T13:16:30+00:00 jouvelot 2021-03-23T13:16:30+00:00 7fa73806c771ad682d0bdca6de01f8d51e1462d1 Sure. Thanks. Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com> 

Sure. Thanks.

Co-authored-by: Kazuhiko Sakaguchi <pi8027@gmail.com>
 Update path.v 2021-03-23T11:55:54+00:00 jouvelot 2021-03-23T11:55:54+00:00 6d51f94b218cae4bd51ba268eff90b7c38c8f627 Typo in documentation. 
Typo in documentation.
 Merge pull request #707 from CohenCyril/ident_name_silence 2021-03-18T00:26:51+00:00 Cyril Cohen 2021-03-18T00:26:51+00:00 8e859e628404c50c8191f30489abf4e799f46f8d Silencing warning deprecated-ident-entry 
Silencing warning deprecated-ident-entry
 Adding sorting on tuples. (#720) 2021-03-14T20:42:34+00:00 jouvelot 2021-03-14T20:42:34+00:00 b26bff45cb80da59a5975318a9d2a7e5425a5713 * Adding sorting on tuples. Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com> 
* Adding sorting on tuples.

Co-authored-by: Cyril Cohen <CohenCyril@users.noreply.github.com>
 Silencing warning deprecated-ident-entry 2021-03-12T21:45:02+00:00 Cyril Cohen 2021-03-04T21:45:19+00:00 be445d437200da5765c972074dd0c0de68562adc 






Merge pull request #708 from CohenCyril/hint_locality_silence
2021-03-11T23:07:05+00:00

Cyril Cohen

2021-03-11T23:07:05+00:00

63007afd537608e64dad3f754bb8d6986a042b17

Silencing Hint Locality warning




Silencing Hint Locality warning






Adding big block matrices
2021-03-08T19:52:27+00:00

Cyril Cohen

2020-08-24T22:21:22+00:00

7db7a5fbce42ff387a5750f9fbde5436a9aab1cc

- with special cases for row, column, and diagonal matrices
- we define an order bijection between the indexing of the whole matrix
  and the indexing of the blocks to preserve triangularity





- with special cases for row, column, and diagonal matrices
- we define an order bijection between the indexing of the whole matrix
  and the indexing of the blocks to preserve triangularity







Adding Order.enum and related definitions and theorems
2021-03-07T01:53:20+00:00

Cyril Cohen

2020-08-24T22:21:22+00:00

dceb926ca83cddecf541934012f6c46eafa6b15f












Silence Hint Locality warning
2021-03-04T21:56:43+00:00

Cyril Cohen

2021-03-04T21:56:43+00:00

081c7c29feb1f4c2e66331a88c273f802c9bc27c












Merge pull request #696 from CohenCyril/sumnB
2021-01-25T10:42:04+00:00

Yves Bertot

2021-01-25T10:42:04+00:00

fb9fb240fe7f6a99035a4db23942cb774458d7a3

Adding lemma sumnB




Adding lemma sumnB