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.
- Make
iStartProof
fail when the proof mode is just re-imported, not re-exported.
(1) would be somewhat nicer as it means the proofmode works "more often".