Kazuhiko Sakaguchi

As we discussed (https://github.com/math-comp/math-comp/pull/1046#discussion_r1409396209), it's better to declare ```coq Bind Scope type_scope with eqType. ``` in the presence of reverse coercions because the carrier of `eqType` is a `Type` and...

Refactor qpoly and poly

4

- Bounded degree polynomials defined in `qpoly.v` and some of their properties can be generalized to semirings. - [The formal power series library](https://github.com/hivert/FormalPowerSeries) by Florent Hivert has its own definition...

Semi-modules and semi-algebras

3

I found that many results in `monalg.v` of multinomials can be generalized to `nmodType` and `semiRingType`. However, module and algebra structures where scalars are a semiring (e.g., polynomials where coefficients...

`[porderMixin of ... by <:]` fails for some aliases such as `seqprod` and `seqlexi`

1

Example: ```coq From mathcomp Require Import all_ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. Record tupleprod_of n (T : Type) := Tupleprod { tpval : seqprod T;...

Declaring a predicate `prop` in a namespace causes a typecheck failure

1

Example: ```coq From elpi Require Import elpi. Elpi Command test. Elpi Accumulate lp:{{ namespace ns { pred pred1. pred prop. } pred pred2. pred2 :- ns.pred1. }}. Fail Elpi Typecheck....

`#[primitive] HB.mixin` breaks the types of constants lifting mixin projections

7

Example: ```coq From Coq Require Import ssreflect ssrfun. From HB Require Import structures. #[primitive] HB.mixin Record AddMonoid_of_TYPE S := { zero : S; add : S -> S -> S;...

We plan to change the type of the display parameter of the order type structures in order.v (see math-comp/math-comp#1166). This PR provides a compatibility layer.

##### Motivation for this change See math-comp/math-comp#1213. ##### Checklist - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` - [ ] added corresponding documentation in the headers Reference: [How to document](https://github.com/math-comp/math-comp/wiki/How-to-document)...

Apparently, the recent introduction of number notations or MC2 triggered a slowdown of compilation. So I suggest doing the following two benchmarks: - A performance comparison (timed diff) of apery...

Proof obligations generated, but not in the proof mode

1

The `Parametricity Recursive` command says "The parametricity tactic generated generated proof obligations. Please prove them and end your proof with 'Parametricity Done'". But it does not open the proof mode....