| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
fiat-crypto/OSX
|
| | |
| |
| |
| | |
Note that we don't look inside -arg for eg -coqlib.
|
| | | |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
We fix as suggested by @JasonGross by reading file names from the
_CoqProject when coq_makefile was invoked with one.
I made coqdep only look at the .v files from _CoqProject because it's
easier this way. Since we're going through the _CoqProject parser we
could have coqdep understand more of it but let's leave that to
another PR (and maybe someone else).
Some projects pass vfiles on the command line, we keep the list of
these files to pass them to coqdep via command line even when there is
a _CoqProject.
Multiple project files is probably broken.
|
| |/ |
|
| |
|
|
|
| |
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
Plugin-writers can now use:
-bypass-API
parameter with "coq_makefile".
The effect of that is that instead of
-I API
the plugin will be compiled with:
-I config" -I dev -I lib -I kernel -I library -I engine -I pretyping -I interp -I parsing -I proofs -I tactics -I toplevel -I printing -I intf -I grammar -I ide -I stm -I vernac
|
| | |
|
| | |
|
|
|
The .mli only acknowledges the current API. I'm not guilty your honor!
|
Maxime Dénès
Gaëtan Gilbert
Théo Zimmermann
Enrico Tassi
Pierre-Marie Pédrot
Matej Košík