Pierre-Yves Strub

Removing `dffun` in favor of `ffun`?

6

Quoting `finfun.v` documentation: > {ffun fT} inherits combinatorial structures of rT, i.e., eqType, choiceType, countType, and finType. However, due to some limitations of the Coq 8.9 unification code the structures...

WIP: eudoxus reals

4

Because it's fun.

Add support for YAML + option for non-strict mode + change sections behaviour

9

See issue #40.

The notation [`x] badly interact with the [] selector and the notation for the norm.