Quentin VERMANDE
Quentin VERMANDE
Until now, the algorithm unfolded terms blindly and instantiated an evar with whatever term was on the other side. Now, we remember the terms from the initial unification problem, and...
##### Motivation for this change fixes #1389 Removes a few `HB.instance` that do not declare new instances. ##### Minimal TODO list - [ ] added changelog entries with `doc/changelog/make-entry.sh` -...
##### Motivation for this change This changes the hierarchy in `fingroup.v` so that it relies on the one in `monoid.v`. ##### Minimal TODO list - [ ] added changelog entries...
##### Motivation for this change https://github.com/math-comp/math-comp/pull/1256 left copies of the theory of nmodules and zmodules in `ssralg.v`. This PR removes them and generalizes a few things. FIXME: We now have...
Since algebraic structures that contain only operations (e.g. `magmaType`, `baseUMagmaType` once https://github.com/math-comp/math-comp/pull/1256 is merged) do not depend on `choiceType`, we can/should build instances for function types.
##### Motivation for this change As of now, the characteristic of a ring is always prime, which does not really make sense in general (e.g. for `'Z_4`). This is fixed...
https://github.com/rocq-prover/rocq/pull/20730 finds more general solutions to a certain class of unification problems, so with the eta-expansion in `lift_wf_term_it_impl`, some evars never get instantiated when applying the lemma.
https://github.com/coq/coq/pull/19987 refolds terms before using them to instantiate evars, which can make failing unifications worse than they were before. This PR avoids a few failing rewrites by putting succeeding ones...
I just tried compiling `elpi` with `ppxopt 0.36.0` and it fails because `Pexp_fun` does not exist anymore. Switching to `ppxopt 0.35.0` works.
##### Motivation for this change Resurrection of https://github.com/math-comp/analysis/pull/204. fyi: @mkerjean ##### Checklist - [x] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [x] added corresponding documentation in the headers Reference: [How to...