Kazuhiko Sakaguchi
Kazuhiko Sakaguchi
Related discussion: https://github.com/math-comp/math-comp/pull/381#discussion_r320603902
This PR looks good to me except for the above minor suggestion and CI, but I have an impression that I don't understand Boolean predicates of MathComp deep enough. It...
As information for other coq-elpi users, I'd like to record that this workaround does work: ```coq Elpi Program tutorial lp:{{ /*(*/ kind person type. type mallory, bob, alice person. /*)*/...
@gares Unfortunately, that one doesn't work because PG removes newlines from the input before passing it to coqtop... (So we cannot use line comments in Coq PG. ~Could this be...
"Undeclared scope" and "duplicate clear" warnings are introduced in Coq 8.10. If we continue to "support at least three recent versions," we can get rid of them after the release...
FTR, my PR coq/coq#13909 reduces 3 pairs of ambiguous paths in ssralg. ```diff @@ -1,30 +1,23 @@ Warning: New coercion path [GRing.subring_closedM; GRing.smulr_closedN] : GRing.subring_closed >-> GRing.oppr_closed is ambiguous with...
Those definitions in MathComp are opaque and do not compute, but [CoqEAL](https://github.com/coq-community/coqeal) allows for automatically refining those proof-oriented objects to computation-oriented objects. In the README of CoqEAL, you can find...
@CohenCyril Do you plan to have orthogonal complementation of vector subspaces here?
Hello. Sorry for multi-posting but I implemented [`ring` and `field` tactics for MathComp](https://github.com/math-comp/algebra-tactics) (NB: This is highly experimental and everything is subject to change) with help from Assia and Enrico....
According to coq/coq#9856, we are probably able to use `zify` directly for `ssrnat` and `ssrint` by declaring some class instances (in Coq 8.11 or later).