Kazuhiko Sakaguchi

A smaller example of #257

1

@gares Here it is. You may hijack this PR to fix the issue.

Declaring dual `bPOrderType` and `tPOrderType` instances fails

15

Here is a complete example: ```coq From HB Require Import structures. HB.mixin Record IsPOrdered T := { le : T -> T -> bool }. HB.structure Definition POrder := {...

`#[primitive_class]` makes `HB.structure` diverging

6

Here is a minimal example, but I couldn't identify the reason: ```coq From HB Require Import structures. HB.mixin Record M A := {}. #[primitive_class] HB.structure Definition S := { A...

Replace mdframed with tcolorbox

2

The mdframed package has the issues that [the `skipbelow` parameter does not work](https://github.com/marcodaniel/mdframed/issues/12) ([patch](https://tex.stackexchange.com/questions/292083/mdframed-and-skipbelow/292090#292090)) and that it has not been updated for 10 years now. Here I propose to replace...

Add the wide algorithm* environment and make its caption style consistent with kaobook

3

This PR depends on #225. I will provide an example if needed.

The horizontal alignment of margin notes in framed theorem-like environments when combined with XeLaTeX

1

### Description An extra indentation appears only when we combine kaobook with XeLaTeX. ### Minimal Working Example ```latex \documentclass[ a4paper, fontsize=10pt, twoside=false, secnumdepth=2, numbers=noenddot, fontmethod=tex, ]{kaobook} \usepackage[framed]{kaotheorems} \begin{document} Some text.\marginnote{marginnote...

##### Motivation for this change This PR is the revival of #464 based on MC2. Closes: #464 ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` -...

Add semi-modules, semi-algebras, and semilinear functions

27

##### Motivation for this change Closes #1124 ##### Overlay PRs - ~math-comp/analysis#1271~ (We no longer need it.) ##### Things done/to do - [ ] added corresponding entries in `CHANGELOG_UNRELEASED.md` -...

Should `f \min g` and `f \max g` notations be defined in `function_scope` ?

3

https://github.com/math-comp/math-comp/blob/082c28dc6562c3d947d52b74bd2a6bb592941562/mathcomp/ssreflect/order.v#L1265-L1266 It also seems to apply here: https://github.com/math-comp/math-comp/blob/082c28dc6562c3d947d52b74bd2a6bb592941562/mathcomp/algebra/ssralg.v#L6203-L6210

Incoherence of the implicit status of lemmas

7

As we noticed in #1126, maximally-inserted and non-maximally-inserted implicit arguments are mixed in `GRing`, e.g., ```coq Arguments GRing.addrA {s} x y z. Arguments GRing.addrAC [V] x y z. ``` I...