coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Adding test for bug #3786.	Pierre-Marie Pédrot	2015-02-11
\|
*	Revert "Update test for #3363 now that Require is forbidden inside modules."	Maxime Dénès	2015-01-17
\| \| \| \|	This reverts commit 1c6e7d3744d101124ed0152c2aac1e71c9f9d40d.
*	Update test for #3363 now that Require is forbidden inside modules.	Maxime Dénès	2015-01-12
\|
*	Fixing wrong notation level in #3295.	Hugo Herbelin	2014-12-19
\|
*	#3828 is solved.	Hugo Herbelin	2014-12-16
\|
*	Moving #2447 (congruence) to fixed.	Hugo Herbelin	2014-12-16
\|
*	New reproduction cases for the test suite.	Xavier Clerc	2014-12-11
\|
*	Commits on evar-evar unification fixed HoTT_coq_106 and improved the	Hugo Herbelin	2014-12-05
\| \| \| \| \|	status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
*	Adding test for bug #3417.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test for bug #3487.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test of bug #3682.	Pierre-Marie Pédrot	2014-11-30
\|
*	Bug #3804 is actually closed (thanks to Jason Gross for the notification).	Xavier Clerc	2014-11-25
\|
*	Tweak some test cases.	Xavier Clerc	2014-11-25
\|
*	Adding test for bug #3248.	Pierre-Marie Pédrot	2014-11-24
\|
*	Cleaning up closed bugs in test-suite.	Pierre-Marie Pédrot	2014-11-21
\|
*	Add missing "Fail" to test case for bug #2814.	Xavier Clerc	2014-11-14
\|
*	Reproduction cases for the test suite.	Xavier Clerc	2014-11-14
\|
*	Test #3655 was failing due to an anomaly. Now it rather has to fail	Hugo Herbelin	2014-11-08
\| \| \| \|	normally, so failure is now detected by removing the "Fail".
*	Test fixed by PMP's commits from Oct 21.	Hugo Herbelin	2014-11-08
\|
*	test suite: some reproduction cases for recently-reported bugs.	Xavier Clerc	2014-11-04
\|
*	New bugs revealed fixed: #3408 by (probably) Maxime's commits	Hugo Herbelin	2014-11-03
\| \| \| \| \| \|	on vm and #3068 by Nov 2 commit on destruct. Also fixed test for failure of #3459.
*	More precise test for #3459.	Hugo Herbelin	2014-10-21
\|
*	Bug fixed by Hugo.	Matthieu Sozeau	2014-10-16
\|
*	Adding a timeout to bug #2447.	Pierre-Marie Pédrot	2014-10-15
\|
*	Fix for bug #3618.	Matthieu Sozeau	2014-10-15
\| \| \| \| \|	Fix typeclass resolution which was considering as subgoals of a tactic application unrelated pre-existing undefined evars.
*	Bug 3692 is fixed.	Matthieu Sozeau	2014-10-15
\|
*	Bug 3628 is fixed.	Matthieu Sozeau	2014-10-15
\|
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-10-03
\|
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-30
\|
*	In evarconv and unification, expand folded primitive projections to	Matthieu Sozeau	2014-09-29
\| \| \| \| \| \| \| \| \| \|	their eta-expanded forms which can then unfold back to the unfolded primitive projection form. This removes all special code that was necessary to handle primitive projections before, while keeping compatibility. Also fix cbn which was not refolding primitive projections correctly in all cases. Update some test-suite files accordingly.
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(but deactivated still). Set Keyed Unification to activate the option, which changes subterm selection to _always_ use full conversion _after_ finding a subterm whose head/key matches the key of the term we're looking for. This applies to rewrite and higher-order unification in apply/elim/destruct. Most proof scripts already abide by these semantics. For those that don't, it's usually only a matter of using: Declare Equivalent Keys f g. This make keyed unification consider f and g to match as keys. This takes care of most cases of abbreviations: typically Def foo := bar and rewriting with a bar-headed lhs in a goal mentioning foo works once they're set equivalent. For canonical structures, these hints should be automatically declared. For non-global-reference headed terms, the key is the constructor name (Sort, Prod...). Evars and metas are no keys. INCOMPATIBILITIES: In FMapFullAVL, a Function definition doesn't go through with keyed unification on.
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
\| \| \| \| \| \| \| \|	so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-26
\|
*	Add missing "Fail" to bug cases.	Xavier Clerc	2014-09-26
\|
*	Bug #3566 is fixed.	Xavier Clerc	2014-09-26
\|
*	Add several reproduction files for bugs.	Xavier Clerc	2014-09-25
\|
*	Update test-suite files.	Matthieu Sozeau	2014-09-24
\|
*	Update test-suite files after last commit. Add a file for rewrite_strat	Matthieu Sozeau	2014-09-17
\| \| \| \|	examples.
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
\| \| \| \| \| \| \| \|	contortions in internalization/externalization. It uses a fully typed version of detyping, requiring the environment, to move from primitive projection applications to regular applications of the eta-expanded version. The kernel is unchanged, and only constrMatching needs compatibility code now.
*	Fix test-suite files, and move some opened to closed.	Matthieu Sozeau	2014-09-11
\|
*	Status error for bug #3459.	Pierre-Marie Pédrot	2014-09-04
\|
*	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 test-suite file.	Matthieu Sozeau	2014-08-18
\|
*	Restrict eta-conversion to inductive records, fixing bug #3310.	Matthieu Sozeau	2014-08-14
\|
*	Fix evarconv not applying eta when it used to. Fixes bug#3319.	Matthieu Sozeau	2014-08-08
\|
*	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
\|
*	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.