blob: 83937390fc46bf3bd9500c4014a47cf920c17a51 (
plain)
1
2
3
4
5
6
7
8
|
- **Added:**
`coqc` now provides the ability to generate compiled interfaces.
Use `coqc -vos foo.v` to skip all opaque proofs during the
compilation of `foo.v`, and output a file called `foo.vos`.
This feature is experimental. It enables working on a Coq file without the need to
first compile the proofs contained in its dependencies
(`#8642 <https://github.com/coq/coq/pull/8642>`_ by Arthur Charguéraud, review by
Maxime Dénès and Emilio Gallego).
|
