Pierre-Marie Pédrot

Technically, it shouldn't even be the responsibility of the hint writer, because this super-global behaviour is clearly a bug...

Please open the issue.

These are two different issues though. 1. Uniform naming or namespacing of schemes 2. Allowing to (re)bind schemes to arbitrary definitions. The second point is fairly easy to implement, but...

@spitters do you mean proof-irrelevance rather than UIP? In that case there are some use-cases for impredicative set (which is still part of the kernel of Coq AFAIK) geared towards...

@maximedenes Ltac2 exports a backwards compatibility layer with Ltac1. I guess this could be shipped separately, but for the time being I don't see it making full secession.

I really like this idea, but as usual the devil is in the details. I wouldn't be surprised if we discovered while implementing the CEP that something prevents this to...

I think that treating section variables as constants is the way to go. Instead of having two lists of contexts in the proof engine, we could simply instantiate the toplevel...

We should probably schedule a meeting to talk about this CEP.

> Who wants to have a working group about it? Count me in.

@CohenCyril can I get one as well?