Maxime Dénès

> One way we could indeed improve the vernac with less disruption would be to version it; in that case I'd be OK with having better bracketing of vernacs and...

Thanks for initiating a CEP on this topic! Here's some feedback. Issue 1: I'd introduce a specific syntax for `Proj`-based projections. It could be `x.(f)` or something else. Side question:...

Why not write `Definition f' params (x : R params) := x.(f)` in this case? I.e. putting type annotations should work reasonably ok, no? I had the feeling that having...

@ppedrot Why do you say it will fail? It seems to work fine.

> In the title of the CEP and in Maxime's talk, this proposal is advertised as "proof modes". > > The general idea of having a built-in mechanism to implement...

I think it's a very good idea to start a CEP on this! I can't contribute much at this point, except for the weak head evaluation strategy for which I...

> it just expands an existing scheme Sure, Ltac already does it, so let's do it more. What could go wrong? 

> IIRC most tests are not run via coqc but rather coqtop... can native be triggered in this case? No, indeed. IMHO the test suite should generate `.vo` files, also...

Good point, I'll open an issue so that we can discuss it.

The `coq_makefile` test for latex is very strange: it runs only if `pdflatex` is found. IMHO the test should either be made to depend on latex or never run it.