Yves Bertot

I am workiing on a patch to fourcolor so that it is compatible with this change. There are good chances that the patch will be backward compatible.

I came to a similar conclusion.

I have been trying to construct a minimal example, but I can't reproduce the problem in a few lines yet.

In the meantime shouldn't this PR be re-affected to milestone 1.13.0?

How is that an unfold? The problem is that the command confuses the target expression for the pattern where it should be applied (a user error), but the actual verification...

I am sorry I am so late in the conversation. I was too busy. Yes, @CohenCyril you are right, this example shows a problem in unfold. I always intended to...

I have a hard time understanding what we want to improve here. In my version of Coq using math-comp.1.11+beta1 the following works: `Check can_inj opprK.` Using `About` you see that...

Examples of possible notation could be `*?*` or `?*` or `?...` or `_*`

I agree. I added an example in example/Basics.v to illustrate the `inspect` pattern, but programming with it is error-prone.

Here is a proposition for syntax: Equations test (n : nat) : {n = 0} + {n 0} := test n with_inspect (Nat.eqb n 0) as eq_name => { test...