Quentin VERMANDE
Quentin VERMANDE
The notation `\min_(i
##### Motivation for this change fixes #1257 ##### Minimal TODO list - ~~[ ] added corresponding entries in `CHANGELOG_UNRELEASED.md`~~ - ~~[ ] added corresponding documentation in the headers~~ - [x]...
On `master`, when I do `From mathcomp Require Import fingroup ssralg` I get the error `Level 2 is already declared to have right associativity while it is now expected to...
https://github.com/math-comp/math-comp/pull/1256 changes the behavior of rewrite (seemingly because it generalizes some operations). This PR makes the necessary changes to keep compiling. The CI is supposed to fail because we need...
https://github.com/math-comp/math-comp/pull/1256 generalizes operations. This PR generalizes everything that was on `nmodType` to `baseAddUMagmaType` (and addition to `addMagmaType`). It also changes the `mem` predicate in `common.elpi` to use `coq.unify-eq` because `elpi`'s...
https://github.com/math-comp/math-comp/pull/1169 removes `PartialCancel` that `algR.v` used to define an order on `algR`. We use `copy` instead.
Saves the head constant of a term before delta-reducing it, to be used during canonical structure resolution and to find matching heads. Also prevents trying to solve canonical structure problems...
There is a rewrite that triggers a higher order unification problem whose RHS changes due to https://github.com/coq/coq/pull/19987. The rewrite was not actually needed, so I bypassed it.
----- ### Issue Summary Typesetting `\[a_{\sum_b c}\]` produces an error `Uncaught (in promise) TypeError: o is null`. ### Steps to Reproduce: Compiling the following LaTeX file ``` \documentclass{article} \begin{document} \[a_{\sum_b...
Unifying structures is very slow (see e.g. https://github.com/math-comp/math-comp/pull/1365). So whenever we see a projection, we can try to reduce it. This also simplifies the Canonical Structures procedure (e.g. gets rid...