Quentin VERMANDE
Quentin VERMANDE
It is possible to make clauses using section variables survive the end of the section, contrary to what is stated in the documentation of `coq.elpi.accumulate`. ```coq From elpi Require Import...
The modes of a class are ignored during a typeclass search when the solver does a recursive call. ``` From elpi Require Import elpi tc. #[mode(i)] TC.Declare Class C (n...
When we introduce a term using quotations, it gets introduced using the compatibility constant of primitive projections, rather than the primitive projections themselves. ```coq From elpi Require Import elpi. Set...
If we feed a term to the typeclass solver, which is not exactly of the expected form, then the latter fails. A funny example of this is when a variable...
`mixin-instance-type->mixin-src` produces clauses `mixin-src` clauses that call the unification, without giving the type of the evars it creates. This can lead to a unification of the form `S.sort ?a =...
When HB declares a join for structures with primitive projections, it uses the compatibility constants of the projections instead of the projections themselves. However, the canonical structure table differentiates them,...
As reported by @mkerjean [on Zulip](https://coq.zulipchat.com/#narrow/channel/237666-math-comp-analysis/topic/HB.20error.20message/near/498147591), we have an issue when some key has an instance for some mixin which is valid for any value of some parameter and we...
[Here](https://github.com/Tragicus/analysis/blob/993f46e6a3178f0da38b1359c423d2529c97917a/theories/numfun.v#L418), `HB.howto` does not find the instances on `FImFun.type` (as witnessed immediately after). Besides, the second `Check` fails for unknown reasons, but this might be unrelated to HB.
We need a way to deprecate something that was declared with HB.
The joins `HB` declares depend on the name of the structures, which breaks things when we want to rename structures. Here is a MWE, where the first `Check` uses the...