coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-02-01	[toplevel] Split interactive toplevel and compiler binaries.	Emilio Jesus Gallego Arias
	We make `coqc` a truly standalone binary, whereas `coqtop` is restricted to interactive use. Thus, `coqtop -compile` will emit a warning and call `coqc`. We have also refactored `Coqargs` into a common `Coqargs` module and a compilation-specific module `Coqcargs`. This solves problems related to `coqc` having its own argument parsing, and reduces the number of strange argument combinations a lot.
2018-04-05	Improve shell scripts	zapashcanon

2017-05-10	Moving code for miscellaneous tests to specific files.	Hugo Herbelin
	The rule is that any file misc/*.sh will now be automatically executed from the test-file directory with appropriate environment variables set. The test can use any auxiliary material which is put in a directory of the same name as the test. This avoids making the main Makefile more or more complex. We loose some customization though (no more custom messages such as printing of the number of universes in the test about the number of necessary universes). We could preserve such customization if needed but I did not consider it was worth the effort. Warning: specific targets universes, deps-order, deps-checksum are removed by consistency. Do instead "make misc/universes.log", etc., or even "make misc" for all.