coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Document the changes to IZR.	Guillaume Melquiond	2017-03-22
\|
*	CHANGES: choice over setoids and prop. ext.	Hugo Herbelin	2017-03-03
\|
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-01-19
\|\
\| *	A few words in CHANGES.	Maxime Dénès	2016-12-07
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\|
\| *	Fix some documentation typos.	Guillaume Melquiond	2016-11-24
\| \| \| \| \| \| \| \| \| \|	Note: "dependant" does exist, but it is a noun and it means a person that is somehow financially dependent on someone else.
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	[doc] Mention XML protocol on changes.	Emilio Jesus Gallego Arias	2016-11-16
\| \| \| \| \| \| \| \|	It may be worth it, also added a note about file reorganization.
\| *	Remove the list of bug fixes from CHANGES.	Maxime Dénès	2016-11-14
\| \| \| \| \| \| \| \| \| \|	We could not produce an exhaustive list of such fixes, and the usefulness of such a list is not clear.
\| *	Update CHANGES and credits for 8.6beta1.	Maxime Dénès	2016-11-10
\| \|
\| *	Mention notypeclasses refine in CHANGES	Matthieu Sozeau	2016-11-07
\| \|
\| *	CHANGES for this branch.	Matthieu Sozeau	2016-11-07
\| \|
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-10-26
\| \|\
\| \| *	Revert "Fixing call to "lazy beta iota" in "refine" (restoring v8.4 behavior)."	Maxime Dénès	2016-10-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reverts commit c9c54122d1d9493a965b483939e119d52121d5a6. This behavior of refine has changed three times in recent years, so let's take the time to make up our mind and wait for a major release. Btw, onhyps=None is not a sane way to express that a tactic should be applied to all hypotheses.
\| \| *	Update CHANGES.	Maxime Dénès	2016-10-25
\| \| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-12
\|\\| \|
* \| \|	Allocating a section in CHANGES for changes specific to 8.7.	Hugo Herbelin	2016-10-12
\| \| \|
\| * \|	Tentatively preparing to add changes specific to v8.7 (see PR #275).	Hugo Herbelin	2016-10-12
\|/ /
* \|	Report about changes of semantics of auto as an ltac argument (see #4966).	Hugo Herbelin	2016-10-08
\| \|
* \|	Remove the Set Verbose Compat option and turn the warning on by default.	Maxime Dénès	2016-10-06
\| \| \| \| \| \| \| \| \| \|	These warnings can now be configured like any other, so we don't need a specific option anymore.
* \|	Document change related to Keep Proof Equalities in CHANGES.	Maxime Dénès	2016-10-03
\| \|
* \|	Being more informative about the change of behavior of "subst".	Hugo Herbelin	2016-09-29
\| \|
* \|	Fix description of change in intro semantics.	Maxime Dénès	2016-09-21
\| \|
* \|	Extending "contradiction" so that it recognizes statements such as "~x=x" or ↵	Hugo Herbelin	2016-09-15
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5.
* \|	Refolding: disable in 8.4 compat file, document	Matthieu Sozeau	2016-09-12
\| \|
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\|\\|
\| *	Fixing CHANGES.	Hugo Herbelin	2016-08-17
\| \| \| \| \| \| \| \| \| \|	Option Standard Proposition Elimination Scheme from 8.5 was not documented in the right section.
* \|	Documenting fix of #3070 (subst and chain of dependencies).	Hugo Herbelin	2016-08-17
\| \|
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\|\\|
\| *	Fix #5000: Document the native compiler soundness bug due to Unicode mangling.	Pierre-Marie Pédrot	2016-08-07
\| \|
\| *	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
\|\\|
\| *	Update CHANGES about #3886 bugfix	Matthieu Sozeau	2016-07-29
\| \|
\| *	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
\| \|
\| *	Update CHANGES about critical bugfix and others	Matthieu Sozeau	2016-07-26
\| \|
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-20
\|\\|
\| *	Update CHANGES	Matthieu Sozeau	2016-07-20
\| \|
* \|	Update CHANGES	Matthieu Sozeau	2016-07-20
\| \|
* \|	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).
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-13
\|\\|
\| *	Add a few fixes in CHANGES that were forgotten.	Maxime Dénès	2016-07-08
\| \| \| \| \| \| \| \|	We should really automate the generation of the log of fixes for CHANGES.
* \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-07-07
\|\\|
\| *	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.
* \|	Merge branch 'v8.5' into trunk	Maxime Dénès	2016-07-04
\|\\|
* \|	Update CHANGES, the bugfixes for 4527 and 4726 are	Matthieu Sozeau	2016-07-04
\| \| \| \| \| \| \| \|	not in pl2.
\| *	Mention more fixes in CHANGES before we release pl2.	Maxime Dénès	2016-07-04
\| \|
* \|	Updated CHANGES about subst. More on recursive equations in reference manual.	Hugo Herbelin	2016-06-29
\| \|
* \|	CHANGES: document fix for #4726 too.	Matthieu Sozeau	2016-06-29
\| \|
* \|	CHANGES: document fix for 4527 and compatibility.	Matthieu Sozeau	2016-06-29
\| \|