Cyril Cohen issues

Results 143 issues of


                                            Cyril Cohen

update config

##### Motivation for this change ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` (do not edit former entries, only append new ones, be careful: merge and...

Simplify filters wip

This is an attempt to simplify filters

TODO: MC2 port

WIP: Rewriting countability and finiteness

countability and finiteness now share the interface of `countType` and `finType` through the coercions `countable >-> Sortclass` and `finite >-> Sortclass` e.g. `rpickle c` is replaced by `@pickle [countType of...

experiment :test_tube:

renaming/refactoring :wrench:

TODO: MC2 port

Backport Enrico's inline "!!" refining for the have tactic to mathcomp?

https://github.com/math-comp/analysis/blob/1566e324cd4b56d09a1660521d1c31c3e2ec83da/posnum.v#L20

kind: change math-comp

Solve slowdown in derive

TODO (alternatives): - [ ] Lock the definition of `diff`using a module type : https://github.com/math-comp/analysis/blob/99d2078cc61335967a5c39594b9f2853fe3a8c25/derive.v#L46-L48 - [ ] Use canonical structures instead of typeclasses for automatic derive

"bug" :bug:

enhancement :sparkles:

The notations near and locally are too unstable.

Redo filters in mem_pred style. PR soon!

renaming/refactoring

Could we have a nix upgrade documentation somewhere? (@amahboubi)

a doc on - upgrading the local nix shell (shell.nix) on analysis? - or upgrading the package definitions (mathcomp/extra.nix) on nixpkgs? _Originally posted by @CohenCyril in https://github.com/math-comp/analysis/pull/147#issuecomment-508095855_

documentation :memo:

Cyril Cohen