-
Björn Brandenburg authored
The vernacular commands Opaque / Transparent change coqtop's prompt counter without generating a prompt (for whatever reason). The proof state recorder needs to be aware of this to avoid a out-of-sync assertion false positive.
Björn Brandenburg authoredThe vernacular commands Opaque / Transparent change coqtop's prompt counter without generating a prompt (for whatever reason). The proof state recorder needs to be aware of this to avoid a out-of-sync assertion false positive.