blob: f6120968805e663dcf7e036eeb0dc9c560901dac (
plain)
1
2
3
4
5
6
7
|
- `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).
|
