coq-mathcomp/mathcomp/algebra, branch master

Silencing warning deprecated-ident-entry

2021-03-12T21:45:02+00:00

Merge pull request #708 from CohenCyril/hint_locality_silence

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

Silencing Hint Locality warning

Adding big block matrices

2021-03-08T19:52:27+00:00

- 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

Silence Hint Locality warning

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

Merge pull request #686 from pi8027/drop-coq-8.10

2021-01-22T14:13:52+00:00

Drop support for Coq 8.10

fixes #694

2021-01-18T16:36:20+00:00

Drop support for Coq 8.10 and deprecate the `deprecate` notation

2021-01-15T15:28:21+00:00

- The `deprecate` notation and `iota_add` have been deprecated. All the uses of
  the `deprecate` notation have been replaced with the `deprecated` attribute.
- Deprecation aliases in `ssrnat` and `ssrnum` introduced in MathComp 1.11+beta1
  have been removed.
- Remove `VDFILE` related hacks from `Makefile.common`.

itv_bound comparison with -oo/+oo

2021-01-14T07:49:39+00:00

erroneous deprecation warning

2021-01-04T04:56:16+00:00

Change the interpretation scope of some nullary notations from ring_scope to fun_scope

2020-12-16T13:52:16+00:00