Proof mode only *mostly* works when it is transitively imported, not exported
I was debugging some very strange behavior with @janno yesterday, which turned out to be the following: In iGPS, imports and exports are somewhat... messy. (To be fair, I feel that's a very common problem with Coq developments. I know no best practices.) In particular, there are files that do
From iris.proofmode Require Import tactics, and then other files import that file. That's enough to get notations, because they are always imported, ignoring the usual reexport rules. (Should we report a Coq bug about that? It does not seem necessary.) However, every since @robbertkrebbers recently disabled
Automatic Coercions Imports, this is not enough to get working coercions. So, most tactics worked, but some (e.g.
iCombine) rely on coercions and did not work.
I think we should do one of two things:
- Make the entire proofmode work when it is just re-imported, not re-exported.
iStartProoffail when the proof mode is just re-imported, not re-exported.
(1) would be somewhat nicer as it means the proofmode works "more often".