aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/coqProject_file.ml4
Commit message (Collapse)AuthorAge
* [CoqProject] Add some comments and remove unnecessary use of Pp.Gravatar Emilio Jesus Gallego Arias2018-05-08
| | | | | But indeed we need to split this file, as it is used now from CoqIDE is incorrect.
* Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵Gravatar Maxime Dénès2018-03-09
|\ | | | | | | fiat-crypto/OSX
| * Closes #6830: coqdep reads options and files from _CoqProject.Gravatar Gaëtan Gilbert2018-03-06
| | | | | | | | Note that we don't look inside -arg for eg -coqlib.
| * Add source (project file / command line) to project fields.Gravatar Gaëtan Gilbert2018-03-01
| |
| * Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSXGravatar Gaëtan Gilbert2018-02-28
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
| | | | | | | | | | 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].
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* Forbidding -o and -f in input file of coq_makefile.Gravatar Hugo Herbelin2017-12-23
| | | | This was apparently either silently doing nothing or failing.
* Avoid looping when searching for CoqProject.Gravatar Maxime Dénès2017-09-27
| | | | | | | This could happen with paths on Windows, or even relative paths on all OSs. Fixes #5730: CoqIDE becomes unresponsive on file open.
* coq_makefile: use System.exists_dir for better portabilityGravatar Enrico Tassi2017-07-20
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Add support for "-bypass-API" argument of "coq_makefile"Gravatar Matej Košík2017-06-12
| | | | | | | | | | | | | | | | 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
* coq_makefile: avoid spurious ./ in generated .conf fileGravatar Enrico Tassi2017-05-23
|
* CoqProject_file: document in API deprecated featuresGravatar Enrico Tassi2017-05-23
|
* CoqProject_file: API and code cleanup (tuples -> records)Gravatar Enrico Tassi2017-05-23
|
* ide/project_file.ml4 -> lib/coqProject_file.ml4 + .mliGravatar Enrico Tassi2017-05-23
The .mli only acknowledges the current API. I'm not guilty your honor!
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 07:48:43 +0000