coq - The formal proof system

Age	Commit message (Collapse)	Author
2017-06-10	Remove (useless) aliases from the API.	Matej Košík

2017-06-07	Put all plugins behind an "API".	Matej Kosik

2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
	This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias

2017-05-16	Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.	Hugo Herbelin

2017-04-25	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias
	Now it is a private field, locations are optional.
2017-02-17	Ltac as a plugin.	Pierre-Marie Pédrot
	This commit is essentially moving files around. In particular, the corresponding plugin still relies on a mllib file rather than a mlpack one. Otherwise, this causes link-time issues for third-party plugins depending on modules defined in the Ltac plugin.