| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
|
|
| |
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!
|
Emilio Jesus Gallego Arias
Enrico Tassi
Hugo Herbelin
Maxime Dénès
Pierre-Marie Pédrot
Matej Košík