Cyril Cohen

This tool merges several gitter room json files into one, with an additional room field for each message.

**For mathcomp 1.14.0**, remove `big_uncond` (i.e. the deprecation warning set for 1.13.0 in #589, cf #492) Also remove other 1.13.0 deprecations

WIP galmx : gal_of -> matrix

4

##### Motivation for this change Adding the operator galmx which gives a matrix representation of an element of a galois group. It was used in a -- now deleted --...

Spacing convention before `//`

1

When should we write `thm//` and when should we write `thm //`? Clarify, document in `CONTRIBUTING.md` and uniformize the library.

WIP matrix of a function and base change matrices

1

##### Motivation for this change This file has to be documented. And the names have to be thought about harder. ##### Things done/to do - [ ] added corresponding entries...

[meta-issue] Clanup using features of Arguments

9

#### TODO impl` using `Arguments` option `simpl never`, cf #94. This is "broken" up to Coq 8.13 cf #660 https://github.com/coq/coq/issues/13428) - [ ] Tune `mask` in a better way? (open...

Using Arguments simpl never instead of nosimpl

11

##### Motivation for this change Fixes #94 ##### Things done/to do - ~added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries)~ - ~added corresponding documentation in the headers~ #####...

> @CohenCyril It seems to me that naming inconsistency still exists after this renaming. Do you plan to perform one more step of renamings to make them consistent? https://github.com/coq/coq/blob/2706baf2651da5d425ed8ef77f68c55c809f92fd/theories/ssr/ssrbool.v#L2120-L2125 https://github.com/coq/coq/blob/2706baf2651da5d425ed8ef77f68c55c809f92fd/theories/ssr/ssrbool.v#L2165-L2175...

Adding a CODEOWNERS file

1

##### Motivation for this change Put someone in charge of each file so that we know who will be more efficient writing a review about each PR. This is the...

Work In Progress: adding forms and spectral theorems

4

Content: - Adding bilinear, sesquilinear, hermitian (symmetric, skew symmetric and hermitian) and hermitian positive definite forms. - A proof of the spectral theorem for normal matrices, and some theory of...