| Age | Commit message (Collapse) | Author |
|---|
|
Use `{pred T}` systematically for generic _collective_ boolean
predicate.
Use `PredType` to construct `predType` instances.
Instrument core `ssreflect` files to replicate these and other new
features introduces by coq/coq#9555 (`nonPropType` interface,
`simpl_rel` that simplifies with `inE`).
|
|
|
|
while some refs (see e.g. [1]) don't assume that the "transitive closure" is
reflexive; so one won't need to look at lemma "connect0" to figure this out.
[1] https://en.wikipedia.org/wiki/Transitive_closure
[ci skip]
|
|
```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```
|
|
See the discussion here:
https://github.com/math-comp/math-comp/pull/242#discussion_r233778114
|
|
|
|
|
|
- f_finv
- finv_f
- fconnect_sym
- iter_order
- iter_finv
- cycle_orbit
- fpath_finv (* I need to sub-theorems for this case. *)
All generalizations are named "..._in" the existing theorems are now
instances of the generalizations.
|
|
|
|
|
