coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
\| *	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
\| \|
* \|	Merge remote-tracking branch 'github/pr/207' into trunk	Maxime Dénès	2016-06-28
\|\ \ \| \| \| \| \| \| \| \| \|	Was PR#207: Add -no-print-dependent-evars
\| \| *	Univs/CHANGES: #4097 and annotations on notations	Matthieu Sozeau	2016-06-27
\| \| \|
* \| \|	Update CHANGES and COMPATIBILITY	Matthieu Sozeau	2016-06-27
\| \| \|
* \| \|	Adding ability to put any pattern in binders, prefixed by a quote.	Daniel de Rauglaudre	2016-06-27
\| \| \| \| \| \| \| \| \| \| \| \|	Cf CHANGES for details.
\| * \|	Add [Unset Printing Dependent Evars Line]	Jason Gross	2016-06-19
\|/ / \| \| \| \| \| \| \| \|	This allows a work-around for bug #4819, https://coq.inria.fr/bugs/show_bug.cgi?id=4819.
* \|	Giving a more natural semantics to injection by default.	Hugo Herbelin	2016-06-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	There were three versions of injection: 1. "injection term" without "as" clause: was leaving hypotheses on the goal in reverse order 2. "injection term as ipat", first version: was introduction hypotheses using ipat in reverse order without checking that the number of ipat was the size of the injection (activated with "Unset Injection L2R Pattern Order") 3. "injection term as ipat", second version: was introduction hypotheses using ipat in left-to-right order checking that the number of ipat was the size of the injection and clearing the injecting term by default if an hypothesis (activated with "Set Injection L2R Pattern Order", default one from 8.5) There is now: 4. "injection term" without "as" clause, new version: introducing the components of the injection in the context in left-to-right order using default intro-patterns "?" and clearing the injecting term by default if an hypothesis (activated with "Set Structural Injection") The new versions 3. and 4. are the "expected" ones in the sense that they have the following good properties: - introduction in the context is in the natural left-to-right order - "injection" behaves the same with and without "as", always introducing the hypotheses in the goal what corresponds to the natural expectation as the changes I made in the proof scripts for adaptation confirm - clear the "injection" hypothesis when an hypothesis which is the natural expectation as the changes I made in the proof scripts for adaptation confirm The compatibility can be preserved by "Unset Structural Injection" or by calling "simple injection". The flag is currently off.
* \|	Mentioning goal selectors in CHANGES	Enrico Tassi	2016-06-17
\| \|
* \|	Fix wrong tabulation in CHANGES	Matthieu Sozeau	2016-06-16
\| \|
* \|	Document new Hint Mode option.	Matthieu Sozeau	2016-06-16
\| \|
* \|	Revise syntax of Hint Cut	Matthieu Sozeau	2016-06-16
\| \| \| \| \| \| \| \| \| \|	As noticed by C. Cohen it was confusingly different from standard notation.
* \|	Not taking arguments given by name or position into account when	Hugo Herbelin	2016-06-16
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	computing the arguments which allows to decide which list of implicit arguments to consider when several such lists are available. For instance, "eq_refl (A:=nat)" is now interpreted as "@eq_refl nat _", the same way as if we had said: Arguments eq_refl {A} {x}.