coq - The formal proof system

Age	Commit message (Collapse)	Author
2019-01-30	[toplevel] Deprecate the `-compile` flag in favor of `coqc`.	Emilio Jesus Gallego Arias
	This PR deprecates the use of `coqtop` as a compiler. There is no point on having two binaries with the same purpose; after the experiment in #8690, IMHO we have a lot to gain in terms of code organization by splitting the compiler and the interactive binary. We adapt the documentation and adapt the test-suite. Note that we don't make `coqc` a true binary yet, but here we take care only of the user-facing part. The conversion of the binary will take place in #8690 and will bring code simplification, including a unified handling of arguments.
2018-06-22	Fix #7704: get_toplevel_path needs normalised argv.(0)	Gaëtan Gilbert
	When launched through PATH argv.(0) is just the command name. eg "coqtop -compile foo.v" -> argv.(0) = "coqtop" Using executable_name also follows symlinks but this isn't tested to avoid messing with windows. Running Coq through a symlink is not as important as PATH anyways.