coq - The formal proof system

Age	Commit message (Collapse)	Author
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
	Add headers to a few files which were missing them.
2020-02-24	[exn] Forbid raising in exn printers, make them return Pp.t option	Emilio Jesus Gallego Arias
	Raising inside exception printers is quite tricky as the order of registration for printers will indeed depend on the linking order. We thus forbid this, and make our API closer to the upstream `Printexn` by having printers return an option type.
2020-01-29	[rfc] [mltop] Removal of dynamic loading of object and `.ml` files	Emilio Jesus Gallego Arias
	This seems seldom used and I think in general instrumentation this way is pretty limited (usually better to use the build system to tweak) It thus seems worth removing as to simplify `Mltop` a bit, but of course comments are welcome.
2020-01-16	[mltop] Remove error handling hacks in favor of default methods.	Emilio Jesus Gallego Arias
	We don't need to handle `Dynlink` errors specially anymore.
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.