Attending: Yves Bertot, Pierre Roux, Emilio Jesus Gallego Arias, Théo Zimmermann
Notes
Ambiguous Requires. Shadowing happens already between installed project A and recompiling the local -R A theories for example, we want to still allow this. Gaëtan will try the installed/local flags for ROCQPATH/user-contrib on one side and -R / -Q for local packages to have a hierarchy for detecting dangerous or harmless ambiguities.
Problem with emulating the previous strategy for finding schemes on inductives in Prop (dep or not dependent). To be investigated further by Gaëtan.
Windows CI directly using opam setup. CoqIDE and test-suite hack questions. CoqIDE support can be delayed. test-suite hacks do not seem to worry Emilio and Gaëtan for now. The PR should be finished soon, after Emilio writes a bit of doc.