| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-07-17 | Remove fourier plugin | Maxime Dénès | |
| As stated in the manual, the fourier tactic is subsumed by lra. | |||
| 2018-07-11 | Merge PR #8002: make-both-single-timing-files: fix --sort-by=diff | Jason Gross | |
| 2018-07-08 | Merge PR #8015: Output UTF-8 explicitly in timing tools | Jason Gross | |
| 2018-07-08 | Remove Emacs modes. | Théo Zimmermann | |
| They are not used anymore. People should use Proof-General (and optionally Company-Coq) instead. | |||
| 2018-07-07 | make diff sort by difference, not absolute difference | Ralf Jung | |
| 2018-07-07 | make-both-single-timing-files: fix --sort-by=diff | Ralf Jung | |
| 2018-07-07 | Output UTF-8 explicitly in timing tools | Jasper Hugunin | |
| 2018-07-07 | Merge PR #7921: Archive the `gallina` tool | Maxime Dénès | |
| 2018-07-05 | Merge PR #7990: Convert timing tool to python3 | Jason Gross | |
| 2018-07-05 | Merge PR #7746: Many small cleanups removing unused arguments and functions | Pierre-Marie Pédrot | |
| 2018-07-04 | Convert timing tools to run with both python2 and python3 | Jasper Hugunin | |
| 2018-07-03 | Fix timing tools on NixOS. | Théo Zimmermann | |
| 2018-07-03 | coqdoc Index.find_string: remove unused argument. | Gaëtan Gilbert | |
| Unused since 6832c60f741e6bfb2a850d567fd6a1dff7059393. | |||
| 2018-07-03 | Coq_makefile.generate_conf_coq_config: remove unused argument. | Gaëtan Gilbert | |
| 2018-06-25 | Archive the `gallina` tool | Vincent Laporte | |
| 2018-06-16 | Fix #7836: tools/inferior-coq.el uses next-line instead of forward-line. | Perry E. Metzger | |
| 2018-06-13 | Merge PR #7241: [coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233) | Théo Zimmermann | |
| 2018-05-31 | Explicitly require python2 in python scripts in tools/ | Armaël Guéneau | |
| 2018-05-21 | [ide] Remove special option `-ideslave` | Emilio Jesus Gallego Arias | |
| This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag. | |||
| 2018-05-21 | [stm] Make toplevels standalone executables. | Emilio Jesus Gallego Arias | |
| We turn coqtop "plugins" into standalone executables, which will be installed in `COQBIN` and located using the standard `PATH` mechanism. Using dynamic linking for `coqtop` customization didn't make a lot of sense, given that only one of such "plugins" could be loaded at a time. This cleans up some code and solves two problems: - `coqtop` needing to locate plugins, - dependency issues as plugins in `stm` depended on files in `toplevel`. In order to implement this, we do some minor cleanup of the toplevel API, making it functional, and implement uniform build rules. In particular: - `stm` and `toplevel` have become library-only directories, - a new directory, `topbin`, contains the new executables, - 4 new binaries have been introduced, for coqide and the stm. - we provide a common and cleaned up way to locate toplevels. | |||
| 2018-05-08 | [coqdep] Remove unnecessary dependency on Pp and CError. | Emilio Jesus Gallego Arias | |
| This allows for even earlier bootstrapping. | |||
| 2018-05-08 | [coqdep] Minor cleanups. | Emilio Jesus Gallego Arias | |
| - Remove inclusion of the `tactics` directory, this is coming from a time loadable modules were found there, now all are under `plugins`. - Remove 2 dependencies so we can bootstrap coqdep earlier. - Use `Format` instead of `Printf` for printing. | |||
| 2018-05-04 | Fix #7413: coqdep warning on repeated files | Gaëtan Gilbert | |
| The same warning exists in ocamllibdep so I copied the change there. Detecting when 2 paths are the same is approximate, eg ././a.ml and a.ml are considered different. Implementing realpath probably isn't worth doing for this warning. | |||
| 2018-04-27 | Fix PHONY typo in coq_makefile | Gaëtan Gilbert | |
| 2018-04-13 | [coq_makefile] COQMF_WINDRIVE is empty on linux (fix #7233) | Enrico Tassi | |
| 2018-03-30 | Remove deprecated commands Arguments Scope and Implicit Arguments | Jasper Hugunin | |
| 2018-03-21 | docs | Ralf Jung | |
| 2018-03-20 | coq_makefile: provide variables to override for adding extra flags | Ralf Jung | |
| 2018-03-20 | coq_makefile: FLAG make variables should not contain LIBS | Ralf Jung | |
| 2018-03-09 | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for ↵ | Maxime Dénès | |
| fiat-crypto/OSX | |||
| 2018-03-08 | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | |
| 2018-03-06 | Closes #6830: coqdep reads options and files from _CoqProject. | Gaëtan Gilbert | |
| Note that we don't look inside -arg for eg -coqlib. | |||
| 2018-03-01 | Add source (project file / command line) to project fields. | Gaëtan Gilbert | |
| 2018-02-28 | Fix #6830: coqdep VDFILE uses too many arguments for fiat-crypto/OSX | Gaëtan Gilbert | |
| 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. | |||
| 2018-02-27 | Update headers following #6543. | Théo Zimmermann | |
| 2018-02-19 | Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ↵ | Maxime Dénès | |
| camlp4 | |||
| 2018-02-17 | Change references to CAMLP4 to CAMLP5 to be more accurate since we no | Jim Fehrle | |
| longer use camlp4. | |||
| 2018-02-17 | Implement name mangling option | Jasper Hugunin | |
| 2018-02-15 | Merge PR #1073: new quick2vo target: like vio2vo, but smarter | Maxime Dénès | |
| 2018-02-15 | new quick2vo target: like vio2vo, but smarter | Ralf Jung | |
| 2018-02-15 | Merge PR #6741: coq_makefile: Support "" as the prefix in _CoqProject | Maxime Dénès | |
| 2018-02-15 | coq_makefile: Support "" as the prefix in _CoqProject | Joachim Breitner | |
| This fixes #6350 (and even comes with a test case). Refering to other directories as `-R … ""` is maybe not best practice, but some people out there do it, so as long as it does not cause too much trouble, we can continue to support it. | |||
| 2018-02-13 | Merge PR #6704: Fix coq_makefile not passing -R options to coqdoc, breaking ↵ | Maxime Dénès | |
| links (#6697) | |||
| 2018-02-09 | [error] Replace msg_error by a proper exception. | Emilio Jesus Gallego Arias | |
| 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]. | |||
| 2018-02-07 | Possible fix for issue #6697 | Yannick Forster | |
| 2018-01-16 | Merge PR #6466: Replace md5sum/md5 calls by an OCaml program | Maxime Dénès | |
| 2018-01-15 | Avoid shell backticks and improve md5sum.ml error messages | Jacques-Pascal Deplaix | |
| 2018-01-11 | Added newline at the end of usage of coqdep. | Bernhard Schommer | |
| 2018-01-08 | Merge PR #6516: Add TIMING_SORT_BY and --sort-by to timing scripts | Maxime Dénès | |
| 2017-12-27 | Add TIMING_SORT_BY and --sort-by to timing scripts | Jason Gross | |
| This should help with #5675, in particular with https://github.com/coq/coq/issues/5675#issuecomment-349716292 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |