coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-10-09	[stm] move par: implementation to vernac/comTactic and stm/partac	Enrico Tassi
	The current implementation of par: is still in the STM, but is optional. If the STM does not take over it, it defaults to the implementation of in comTactic which is based on all: (i.e. sequential). This commit also moved the interpretation of a tactic from g_ltac to vernac/comTactic which is more appropriate. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2019-07-08	An even more uniform treatment of the -help option across executables.	Hugo Herbelin
	Incidentally fix some missing newline in coqc help, and give proper help for coqidetop and the "coq*worker"s.
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann

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.