coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Remove reference name type.	Maxime Dénès	2018-06-18
\| \| \| \| \| \| \| \|	reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
*	Remove some occurrences of Evd.empty	Maxime Dénès	2018-05-25
\| \| \| \|	We address the easy ones, but they should probably be all removed.
*	[ide] Remove special option `-ideslave`	Emilio Jesus Gallego Arias	2018-05-21
\| \| \| \| \|	This has no effect anymore, verbose printing is controlled now by the regular, common `quiet` flag.
*	[stm] Make toplevels standalone executables.	Emilio Jesus Gallego Arias	2018-05-21
	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.