coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Added a test file for contradiction.	Hugo Herbelin	2016-09-15
\|
*	Continuing fix to #5078, taking also into account intropatterns.	Hugo Herbelin	2016-09-15
\| \| \| \|	Getting closer from before when the bug was introduced + test.
*	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.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.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
\| \|
* \|	Fix bug #4904: [Import] does not load intermediately unqualified names of ↵	Pierre-Marie Pédrot	2016-08-23
\| \| \| \| \| \| \| \|	aliases.
* \|	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
\| \| \|
* \| \|	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
\| \| \|
\| * \|	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.
\| * \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| \| \|
* \| \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| \| \|
\| * \|	Fix Errors.out missing a dot...	Matthieu Sozeau	2016-07-19
\| \| \|
* \| \|	Some extra fixes in printing patterns in binders.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
* \| \|	Taking into account binding patterns when agglutinating sequences of binders.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Supporting accordingly printing of sequences of binders including binding patterns.
* \| \|	Fixing missing parentheses in printing of patterns in binders.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \|	(In agreement with Daniel.)
* \| \|	Notations: fixing multiple binders used as terms in reverse order.	Hugo Herbelin	2016-07-19
\| \| \|
* \| \|	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The same variable name was used to collect the binders and the successive steps of matching one binder, resulting in unexpected attempts for merging in the presence of multiple occurrence of the same recursive pattern. An amusing side-effect: when eta-expanding for a notation with recursive binders, it is the second variable of the "x .. y" which is used to invent a name rather than the first one.
* \| \|	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).