The Coq mailing list

["Randy Pollack" <rap AT dcs.ed.ac.uk>]

> The gallina file .g is just the version of the vernacular file .v without
> the proofs. Thus, you have the whole development (definitions, syntax,
> lemmas, etc.) but without the hundreds lines of proof.

Sometimes I want to load a .v file, skipping the proofs and treating
the lemmas as axioms.  Coq supports the compiled .vi file for this
purpose, but then you must maintain the .vi files up-to-date ....

Here is a suggestion for a different approach: have a top-level switch
that tells whether or not to load the proofs from a .v file.  If
proofs are not being loaded, then Lemmas are treated as Axioms.
Further, a source specification file, i.e. a .v file without proofs,
could be loaded in this no-proof mode, without changing "Lemma" to
"Axiom".

BTW, the switch could also work for loading .vo files, so there would
no longer be a need for the .vi format at all.  (This might require a
change in .vo format, to distinguish between definitions and proved
lemmas.)  Such a switch is dynamically set and reset, giving more
flexibility than .vi files.

Best regards,
Randy