| Age | Commit message (Collapse) | Author |
|---|
|
|
|
But indeed we need to split this file, as it is used now from CoqIDE
is incorrect.
|
|
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.
|
|
|
|
The current error mechanism in the core part of Coq is 100% exception
based; there was some confusion in the past as to whether raising and
exception could be replace with `Feedback.msg_error`.
As of today, this is not the case [due to some issues in the layer
that generates error feedbacks in the STM] so all cases of `msg_error`
must raise an exception of print at a different level [for now].
|
|
... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
|
|
This was apparently either silently doing nothing or failing.
|
|
This could happen with paths on Windows, or even relative paths on all
OSs.
Fixes #5730: CoqIDE becomes unresponsive on file open.
|
|
|
|
|
|
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!
|
