coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing #5161 (case of a notation with unability to detect a recursive binder).	Hugo Herbelin	2016-10-27
\| \| \| \| \|	Type annotations in unrelated binders were badly interfering with detection of recursive binders in notations.
*	Merge remote-tracking branch 'github/pr/329' into v8.5	Maxime Dénès	2016-10-25
\|\ \| \| \| \| \| \|	Was PR#329: Fix #5127 Memory corruption with the VM
\| *	Test file for #5127: Memory corruption with the VM	Maxime Dénès	2016-10-24
\| \|
* \|	Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").	Hugo Herbelin	2016-10-24
\|/
*	Fix 6d5fe92e to #5150 (missing dependencies in test suite) was a bit too strong.	Hugo Herbelin	2016-10-24
\| \| \| \| \| \| \| \|	New fix. A bit less consistent with the spirit of this Makefile as we list prerequisite files explicitly, but avoid to redo subsystems at each call to "make" as with previous fix. Other solutions from experts are welcome.
*	Fixing printing of generic arguments of tag "var".	Hugo Herbelin	2016-10-22
\|
*	Revert "unification.ml: fix for bug #4763, unif regression"	Maxime Dénès	2016-10-21
\| \| \| \| \| \| \| \|	This reverts commit 0b417c12eb10bb29bcee04384b6c0855cb9de73a. A good fix requires to review a bit the design of unification constraint postponement, which we do in 8.6. We leave things as they are in 8.5 for compatibility.
*	Adding dependency of the test-suite subsystems in prerequisite (fixing #5150).	Hugo Herbelin	2016-10-20
\|
*	A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).	Hugo Herbelin	2016-10-20
\| \| \| \| \| \| \| \| \|	If an existing evar was cleared in pretyping (typically while processing "ltac:"), it created an evar considered as new. Updating them instead along the "cleared" flag. If correct, I suspect similar treatment should be done for refining along "change", "rename" and "move".
*	Removing output test for module qualification.	Pierre-Marie Pédrot	2016-10-18
\| \| \| \| \| \| \| \| \|	I do not know how to provide a proper test in 8.5, as the location on my machine appears in the error printed when loading the file. Adding a Fail on the End command does not help much either, because it simply does not print anything. Do not merge this commit in 8.6, we still want a test there.
*	Fixing to #3209 (Not_found due to an occur-check cycle).	Hugo Herbelin	2016-10-17
\| \| \| \| \| \| \|	The fix solves the original bug report but it only turns the Not_found into a normal error in the alternative example by Guillaume. See test-suite file for comments on how to eventually improve the situation and find a solution in Guillaume's example too.
*	Merge PR #310 into v8.5	Pierre-Marie Pédrot	2016-10-17
\|\
\| *	Test for bug #4874.	Pierre-Marie Pédrot	2016-10-17
\| \|
* \|	Fixing a collision about the meta-variable ".." in recursive notations.	Hugo Herbelin	2016-10-12
\| \| \| \| \| \| \| \| \| \|	This happens when recursive notations are used to define recursive notations.
* \|	Merge remote-tracking branch 'git/bug5123' into v8.5	Matthieu Sozeau	2016-10-12
\|\ \
\| * \|	Fix test-suite file 5123 to fail in case of regression	Matthieu Sozeau	2016-10-11
\| \| \|
\| * \|	Fix bug #5123: mark all shelved evars unresolvable	Matthieu Sozeau	2016-10-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Previously, some splipped through and were caught by unrelated calls to typeclass resolution.
* \| \|	Fix for bug #4863, update the Proofview's env with	Matthieu Sozeau	2016-10-11
\|/ / \| \| \| \| \| \| \| \|	side_effects. Partial solution to the handling of side effects in proofview.
* /	Add test file for #4416.	Maxime Dénès	2016-10-10
\|/
*	evarconv.ml: Fix bug #4529, primproj unfolding	Matthieu Sozeau	2016-10-06
\| \| \| \| \|	Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that.
*	unification.ml: fix for bug #4763, unif regression	Matthieu Sozeau	2016-10-06
\| \| \| \| \| \| \|	Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too.
*	Fixing #4970 (confusion between special "{" and non special "{{" in notations).	Hugo Herbelin	2016-10-03
\|
*	Fix test-suite.	Maxime Dénès	2016-09-30
\| \| \| \|	Restore subst output test file modified by mistake.
*	Merge branch '4762' into v8.5	Maxime Dénès	2016-09-30
\|\ \| \| \| \| \| \|	Was PR#293: Fix #4762 (eauto weaker than auto).
\| *	Fix #4762.	Cyprien Mangin	2016-09-30
\| \|
* \|	Fix a bug in subst releaved by an OCaml warning.	Maxime Dénès	2016-09-29
\|/
*	Fixing #5095 (non relevant too strict test in let-in abstraction).	Hugo Herbelin	2016-09-22
\|
*	Fixing test-suite after commit 43104a0b.	Pierre-Marie Pédrot	2016-09-14
\|
*	Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.	Hugo Herbelin	2016-09-12
\|
*	Test for #5077.	Hugo Herbelin	2016-09-10
\|
*	Test file for #5065 - Anomaly: Not a proof by induction	Maxime Dénès	2016-09-05
\|
*	Fix test-suite after Frédéric's 6231f07b2.	Maxime Dénès	2016-09-01
\|
*	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 an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\|
*	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
\| \| \| \|	Modulo delta for types should be fully transparent.
*	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 #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\|
*	Fix Errors.out missing a dot...	Matthieu Sozeau	2016-07-19
\|
*	Fixing printing of evar name in an error message of instantiate.	Hugo Herbelin	2016-07-13
\|
*	Fix test file for #4858.	Maxime Dénès	2016-07-08
\|
*	Update csdp.cache.	Maxime Dénès	2016-07-08
\|
*	Test file for #4858.	Maxime Dénès	2016-07-08
\|
*	Add test file for #4880.	Maxime Dénès	2016-07-08
\|
*	Update csdp.cache.	Maxime Dénès	2016-07-06
\|
*	Merge remote-tracking branch 'github/pr/199' into v8.5	Maxime Dénès	2016-07-06
\|\ \| \| \| \| \| \|	Was PR#199: Unbreak singleton list-like notation (-compat 8.4)
* \|	congruence fix: test-suite code and update CHANGES	Matthieu Sozeau	2016-07-05
\| \| \| \| \| \| \| \|	This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718.
* \|	congruence: Restrict refreshing to Set	Matthieu Sozeau	2016-07-04
\| \| \| \| \| \| \| \| \| \| \| \|	Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards.
* \|	congruence/univs: properly refresh (fix #4609)	Matthieu Sozeau	2016-07-04
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609.