Quentin VERMANDE
Quentin VERMANDE
##### Motivation for this change Generalizes the instances on function types to dependent function types. The same generalization is happening in mathcomp (see https://github.com/math-comp/math-comp/pull/1256) and it needs to be done...
The unification algorithm sometimes fails on problems of the form `?a = t` because variables that are not in the scope of `?a` appear in `t`. This PR solves the...
Continuity of linear functions in finite dimension ##### Motivation for this change ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the...
##### Motivation for this change This PR adds notions of differential calculus that we want for differential geometry. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [...
##### Motivation for this change Proof of Mertens theorems. This still requires a bit of prettyfiyng, but the proof is complete if someone wants to take a look. Dependecies: -...
There are a few `repeat split` in definitions of groups, which causes `split` to try and solve equalities using reflexivity. This used to fail, but with https://github.com/rocq-prover/rocq/pull/21180 the unification algorithm...
`src/rocq_elpi_utils.ml/detype` now turns identical evars into identical holes. Fixes #919
When a term contains multiple occurrences of an evar, `coq.elaborate-skeleton` produces a fresh unification variable for every occurrence of the evar, e.g. `f ?x ?x` is interpreted as `f _...
The previous version may leave some `tc.maybe-eta-tm` in the terms, which the compiler from elpi terms to rocq terms does not like at all.
It seems that `apply:` calls the typeclass solver on the goal it produces and somehow accepts a partial solution from elpi's typeclass solver. I am surprised both by the fact...