coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing test FunExt.v.	Hugo Herbelin	2016-09-19
\|
*	extensionality: Handle dependently-used hypotheses	Jason Gross	2016-09-19
\|
*	Adding an "extensionality in H" tactic which applies functional	Hugo Herbelin	2016-09-19
\| \| \| \| \| \| \| \|	extensionality in H supposed to be a quantified equality until giving a bare equality. Thanks to Jason Gross and Jonathan Leivent for suggestions and examples.
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-14
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-14
\| \|\
\| \| *	Fixing test-suite after commit 43104a0b.	Pierre-Marie Pédrot	2016-09-14
\| \| \|
\| * \|	test-suite/output-modulo-time made more robust	Enrico Tassi	2016-09-13
\| \| \|
\| \| *	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
\| \| \|
\| * \|	Merge remote-tracking branch 'github-coq/pr/249' into v8.6	Matthieu Sozeau	2016-09-12
\| \|\ \
\| * \| \|	Add support for testing output mod timing changes	Jason Gross	2016-09-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Uses sed 's/\s[0-9]\.[0-9]\+\s//g' and 's/\s0\.\s*//g' to strip numbers of seconds and to strip percentages. (This can potentially be extended later.) Add a test-suite file to make sure that LtacProf outputs some table.
\| * \| \|	Add a test for 4836	Jason Gross	2016-09-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This required improving the machinery of the test-suite Makefile to support -compile.
\| \| \| *	Test for #5077.	Hugo Herbelin	2016-09-10
\| \| \| \|
\| \| * \|	no-refold patch	Paul Steckler	2016-09-09
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add a boolean for refolding during reduction, and an option that is off by default in 8.6, to turn refolding on in all reduction functions, as in 8.5.
\| * \| \|	Fix output test-suite after commit 0d3c319.	Pierre-Marie Pédrot	2016-09-09
\| \|/ /
\| * \|	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 Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
\| \| \| \| \| \| \| \| \| \| \| \|	esprit d'escalier : is now also fixed for R
\| * \|	Fix Bug #5073 : regression of micromega plugin	Frédéric Besson	2016-09-08
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The computed proof term is now more explicit exact (__arith P1 ... Pn X1 ... Xm) instead of apply (__arith P1 ... Pn) which unification could fail.
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-07
\| \|\\|
\| * \|	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
\| \| *	Test file for #5065 - Anomaly: Not a proof by induction	Maxime Dénès	2016-09-05
\| \| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\| \|\\|
\| \| *	Fix test-suite after Frédéric's 6231f07b2.	Maxime Dénès	2016-09-01
\| \| \|
\| * \|	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \|	If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
\| \| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
\| * \|	Fixing output test-suite after warning for inner Requires.	Pierre-Marie Pédrot	2016-08-30
\| \| \|
\| * \|	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
\| \| \|
\| * \|	plugin micromega : nra also handles non-linear rational arithmetic over Q ↵	Frédéric Besson	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
\| * \|	Fix bug #3920: eapply masks an hypothesis name.	Pierre-Marie Pédrot	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch.
\| * \|	Fix bug #4764: Syntactic notation externalization breaks.	Pierre-Marie Pédrot	2016-08-28
\| \| \|
* \| \|	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\\| \|
\| * \|	Fix bug #4904: [Import] does not load intermediately unqualified names of ↵	Pierre-Marie Pédrot	2016-08-23
\| \| \| \| \| \| \| \| \| \| \| \|	aliases.
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-21
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\| \|\\|
\| \| *	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\| \| \|
\| * \|	Test file for bug #4187.	Pierre-Marie Pédrot	2016-08-19
\| \| \|
\| * \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\| \|\ \
\| * \| \|	Adding a test for bug #4653.	Pierre-Marie Pédrot	2016-08-18
\| \| \| \|
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-17
\|\\| \| \|
\| * \| \|	Fixing #3070 ("subst" taking properly into account chains of dependencies).	Hugo Herbelin	2016-08-17
\| \| \| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| \| * \|	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Modulo delta for types should be fully transparent.
\| * \| \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-29
\| \|\\| \|
\| \| * \|	Fix bug #3886, generation of obligations of fixes	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
\| \| * \|	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
\| \| \| \|
* \| \| \|	Merge branch 'v8.6' into trunk	Pierre Letouzey	2016-07-26
\|\\| \| \|
\| \| * \|	Fix bug #4754, allow conversion problems to remain	Matthieu Sozeau	2016-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	when checking that the rewrite relation is homogeneous in setoid_rewrite.
\| * \| \|	Fix bug #4679, weakened setoid_rewrite unification	Matthieu Sozeau	2016-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-07-20
\|\\| \| \|