Quentin VERMANDE

The code below fails, likely (see https://coq.zulipchat.com/#narrow/stream/253928-Elpi-users-.26-devs/topic/Ill-typed.20evar.20instance/near/397185633) due to a bug in coq-elpi. In the following script, I declare `proj1_sig` as a coercion using elpi, then declare some additive structure...

C.axioms_ appears when printing

1

The `axioms_` record of a structure `C` is hidden behind a notation. However, when printing, the notation does not print `C`, as in ``` From HB Require Import structures. HB.mixin...

As mentioned in the corresponding Zulip thread, the following code fails with the error "term->gref: input has no global reference", which is not very clear. Here, `id` should be replaced...

Wochoice

6

(reopening of https://github.com/math-comp/analysis/pull/1173 ) Adds a proof of Zorn's lemma, Hausdorff maximal principle and the well ordering principle. ##### Motivation for this change ##### Checklist - [ ] added corresponding...

Removes algR, which is backported here: - https://github.com/math-comp/math-comp/pull/1199

The lemmas in various.v for the package algebra have been backported here: - https://github.com/math-comp/math-comp/pull/1198

The lemmas in `various.v` for ssralg and poly have been backported here: - https://github.com/math-comp/math-comp/pull/1185 Relies on https://github.com/math-comp/Abel/pull/85

The lemmas in `various.v` for the package ssreflect have been backported here: - https://github.com/math-comp/math-comp/pull/1193 - https://github.com/math-comp/math-comp/pull/1184

The lemmas in various.v for the package algebra have been backported here : - https://github.com/math-comp/math-comp/pull/1196

The lemmas in various.v for the package algebra have been backported here (modulo https://github.com/math-comp/Abel/pull/86): - https://github.com/math-comp/math-comp/pull/1195