coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Fixing injection bug #3616 on sigma-types.	Hugo Herbelin	2014-09-13
\|
*	An old typo which was preventing example #3537 to work the same as it	Hugo Herbelin	2014-09-12
\| \| \| \|	was working in 8.4.
*	Fix test-suite files, and move some opened to closed.	Matthieu Sozeau	2014-09-11
\|
*	Fix bug #3594: eta for constructors and functions at the same time which	Matthieu Sozeau	2014-09-11
\| \| \| \| \|	was failing in this case due to the wrong postponment of an unsolvable ?X = RigidContext[?X] problem.
*	Fix bug #3596, wrong treatment of projections in compute_constelim_direct.	Matthieu Sozeau	2014-09-11
\|
*	Fix bug #3505.	Matthieu Sozeau	2014-09-11
\| \| \| \| \| \| \|	When w_unifying primitive projection applications, force the unification of types of the projected records to recover instances for the parameters (evarconv does this automatically by unifying evar instances with their expected type).
*	Test for "inversion as" naming bug.	Hugo Herbelin	2014-09-07
\|
*	Regression test #3557	Hugo Herbelin	2014-09-07
\|
*	Regression test for bug #2883.	Hugo Herbelin	2014-09-07
\|
*	Fix bug #3584, elaborating pattern-matching on primitive records to the	Matthieu Sozeau	2014-09-06
\| \| \| \|	use of projections.
*	Status error for bug #3459.	Pierre-Marie Pédrot	2014-09-04
\|
*	Test for bug #3459.	Pierre-Marie Pédrot	2014-09-04
\|
*	Fix bug #3561, correct folding of env in context[] matching.	Matthieu Sozeau	2014-09-04
\|
*	Fix bug #3559, ensuring a canonical order of universe level quantifications when	Matthieu Sozeau	2014-09-04
\| \| \| \| \|	introducing constants (e.g. Top.1 is always before Top.2), compatible with the one used before introduction of hMaps in LMap/LSet.
*	Add test suite files for closed bugs.	Matthieu Sozeau	2014-09-04
\|
*	Fix bug #3563, making syntactic matching of primitive projections	Matthieu Sozeau	2014-09-04
\| \| \| \| \|	and their eta-expanded forms succeed, potentially filling parameter metavariables from the type information of the projected object.
*	Test-suite for bug #2818.	Pierre-Marie Pédrot	2014-09-03
\|
*	Add test-suite file. Compute the name for the record binder in the	Matthieu Sozeau	2014-08-29
\| \| \| \|	eta-expanded version of a projection as before.
*	Fix bugs #3484 and #3546.	Matthieu Sozeau	2014-08-28
\| \| \| \| \| \| \|	The unification oracle now prefers unfolding the eta-expanded form of a projection over the primitive projection, and allows first-order unification on applications of constructors of primitive records, in case eta-conversion fails (disabled by previous patch on eta).
*	There are some occurs-check cases that can be handled by imitation (using ↵	Matthieu Sozeau	2014-08-28
\| \| \| \| \| \| \|	pruning), hence do not entirely prevent solve_simple_eqn in case of apparent occurs-check but backtrack to eqappr on OccurCheck failures (problem found in Ssreflect).
*	Adding test-suite for bug #3212.	Pierre-Marie Pédrot	2014-08-28
\|
*	Add a regression test for 3427	Jason Gross	2014-08-26
\|
*	Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possible	Matthieu Sozeau	2014-08-25
\| \| \| \| \|	to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
*	Fix computation of dangling constraints at the end of a proof (bug #3531).	Matthieu Sozeau	2014-08-25
\|
*	Fix test-suite file.	Matthieu Sozeau	2014-08-23
\|
*	Fix test-suite files.	Matthieu Sozeau	2014-08-18
\|
*	Fix test-suite file.	Matthieu Sozeau	2014-08-18
\|
*	Restrict eta-conversion to inductive records, fixing bug #3310.	Matthieu Sozeau	2014-08-14
\|
*	Fix test-suite files according to new parsing rule for application of primitive	Matthieu Sozeau	2014-08-13
\| \| \| \|	projections.
*	Bug #3469: fixing unterminated comment.	Hugo Herbelin	2014-08-12
\|
*	In bug #2406, renouncing to test failure of parsing error.	Hugo Herbelin	2014-08-12
\| \| \| \| \|	(AFAIU, it is the table of supported unicode characters which has to be upgraded anyway.)
*	Fix unification which was failing when unifying a primitive projection against	Matthieu Sozeau	2014-08-09
\| \| \| \|	its expansion if it could reduce (fixes bug #3480).
*	Fix evarconv not applying eta when it used to. Fixes bug#3319.	Matthieu Sozeau	2014-08-08
\|
*	Fixing #3483 (graceful failing with notations to non-constructors in "match").	Hugo Herbelin	2014-08-03
\|
*	Finish fixes on notations and primitive projections, add test-suite files ↵	Matthieu Sozeau	2014-07-31
\| \| \| \|	for closed bugs
*	Add test-suite file for bug #3439.	Matthieu Sozeau	2014-07-30
\|
*	Add test-suite file for bug 3454.	Matthieu Sozeau	2014-07-29
\|
*	Add test-suite file for bug #3453	Matthieu Sozeau	2014-07-29
\|
*	Adding a test-suite for bug #3422.	Pierre-Marie Pédrot	2014-07-21
\|
*	Adding a test-suite for bug #3416.	Pierre-Marie Pédrot	2014-07-16
\|
*	Fix eta expansion of primitive records (HoTT bug #78), which now fails ↵	Matthieu Sozeau	2014-07-03
\| \| \| \| \| \|	cleanly when called on partially applied constructors. Also protect evar_conv from that case.
*	Indeed simpl never is really honored now.	Matthieu Sozeau	2014-07-02
\|
*	Tests for bugs #2834 and #2994.	Hugo Herbelin	2014-06-30
\|
*	Completing test for bug report #2830	Hugo Herbelin	2014-06-30
\|
*	Quickly fixing bug #2996: typing functions now check when referring to	Hugo Herbelin	2014-06-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	a global reference that the current (goal) env contains all the section variables that the global reference expects to be present. Note that the test for inclusion might be costly: everytime a conversion happens in a section variable copied in a goal, this conversion has to be redone when referring to a constant dependent on this section variable. It is unclear to me whether we should not instead give global names to section variables so that they exist even if they are not listed in the context of the current goal. Here are two examples which are still problematic: Section A. Let B := True : Type. Definition C := eq_refl : B = True. Theorem D : Type. clearbody B. set (x := C). unfold C in x. (* inconsistent context ) or Section A. Let B : Type. exact True. Qed. Definition C := eq_refl : B = True. ( Note that this violated the Qed. ) Theorem D : Type. set (x := C). unfold C in x. ( inconsistent context *)
*	Invalid bug report.	Matthieu Sozeau	2014-06-26
\|
*	Fix bug # 3325 using canonical structure declarations where needed.	Matthieu Sozeau	2014-06-26
\|
*	Add an option to disable typeclass resolution during conversion, which	Matthieu Sozeau	2014-06-26
\| \| \| \| \|	is has non-local effects. For now it is not disabled by default, but we'll try to disable it once the test-suite and contribs are stabilized.
*	Merge branch 'tc-test-suite' of https://github.com/JasonGross/coq into ↵	Matthieu Sozeau	2014-06-26
\|\ \| \| \| \| \| \|	JasonGross-tc
* \|	Fixed bug with new semantics of change.	Matthieu Sozeau	2014-06-26
\| \|