Emilio Jesús Gallego Arias

> I am not very convinced by the fact that we really want a vi file separate from the v file in Coq I am very convinced we don't want...

Hi folks, I've added a topic to schedule a possible meeting https://coq.zulipchat.com/#narrow/stream/314095-Coq-Hackathon.20and.20Working.20Group.2C.20Winter.202022/topic/.2Evi.20Interfaces.20Proposal

> Could we sketch an attribute-based solution? Indeed I have a feeling similar to @maximedenes , but I don't know enough yet about the problem. I am in particular missing...

I did give to this some more thought, and I think that we should not use files to track leakage, but the document model should take care of it, as...

Sorry for missing the call today; it seems to me that removing the current mechanism will have a huge impact in terms of compat; on the other hand I don't...

> My own estimation of the cost of porting is "pretty small". Well, just the amount of documentation / tutorials, stuff like SF that needs to be adapted seems to...

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 a...

First question IMO to ask here is why DAP doesn't work for Coq, and how we need to differ from it.

@jfehrle maybe you chose that strategy, but certainly me and other devs don't agree with it, if I understand correctly. You can think DAP is not relevant to the current...

Thanks for the CEP @proux01 , a few comments: - I think that the CEP covers two orthogonal set of tasks, namely: + splitting the stdlib into several packages +...