diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-24 18:45:40 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-09-25 11:19:08 +0200 |
| commit | b6725a2d0077239e51385a62a526ab9465eea26d (patch) | |
| tree | 7af2a0e3fe9b3a4c40b1e46de9e1211ec0e859cb /library/keys.mli | |
| parent | 2ba2ca96be88bad5cd75a02c94cc48ef4f5209b7 (diff) | |
The -compile option now accepts ".v" files and outputs a warning otherwise.
Diffstat (limited to 'library/keys.mli')
0 files changed, 0 insertions, 0 deletions