Kazuhiko Sakaguchi

Added. I wonder if we can make maximally-inserted implicit arguments default (although it might be too aggressive).

I guess what I'm looking for is [`Set Maximal Implicit Insertion`](https://coq.inria.fr/doc/V8.18.0/refman/language/extensions/implicit-arguments#coq:flag.Maximal-Implicit-Insertion).

We discussed this issue during a MathComp dev meeting. Conclusion: let's try `Set Maximal Implicit Insertion` and see how much it breaks stuff.

Apparently, `Set Maximal Implicit Insertion` turns some arguments that come from higher-order predicates maximal implicit. It seems to be too much and they should be non-maximal implicit (so that we...

IIUC, Coq decides the implicit status of an argument (like `x` and `y` above) by looking at the type of the declaration (like `anti_leq`). What we need is 1) to...

Do we need to continue backporting stuff from MC2 to MC1 now? [Trajectories](https://github.com/math-comp/trajectories) is probably the only active project still depending on MC1. Asking the MC users this question tomorrow...

I mean, refreshing my memory about `poly.v` would be useful for refactoring `qpoly.v`. By taking a closer look at a file, I often spot some improvements. At the very least,...

While working on #1237, I found that the `%|` notation in `algC.v` has its own mechanism to cast `nat` and `int` to `algC`. Does this PR eventually allow us to...

This change does not seem to fix the issue completely. If I do: ```coq Arguments intmul [R] x%ring_scope n%int_scope. Set Printing All. Check (10 * 10)%:~R. ``` I get: ```coq...

I think we expect that `int_scope` is a "subscope" (whatever that means) of `ring_scope` because we want to use notations for both scopes in the context expecting a term of...