coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fix coq_makefile uninstall target under OSX.	Maxime Dénès	2017-06-01
\|
*	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\| \| \| \| \| \| \| \|	This allows a better control on the name to give to an evar and, in particular, to address the issue about naming produced by "epose proof" in one of the comment of Zimmi48 at PR #248 (see file names.v). Incidentally updating output of Show output test (evar numbers shifted).
*	Adding tests for testing exit status and #use"include".	Hugo Herbelin	2017-05-10
\|
*	Merge remote-tracking branch 'github/pr/319' into v8.6	Maxime Dénès	2016-10-28
\|\ \| \| \| \| \| \|	Was PR#319: More error tagging, try to fix bug 5135
* \|	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
\|/ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add a lot of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs.
*	Update csdp cache.	Pierre-Marie Pédrot	2016-09-09
\| \| \| \|	This was making the test-suite fail on machines where csdp was not installed.
*	Fix test-suite after Frédéric's 6231f07b2.	Maxime Dénès	2016-09-01