coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixing the anomaly in bug #3045 (a filter was not type-safe in	Hugo Herbelin	2014-10-08
*	Add test-suite file for the projection unfolding bug I just fixed.	Matthieu Sozeau	2014-10-07
*	Fix test-suite file 3352 which was containing the wrong test.	Matthieu Sozeau	2014-10-07
*	Fix test-suite file to test original bug, not the failure of the guard	Matthieu Sozeau	2014-10-07
*	A few improvements on pattern-matching compilation.	Hugo Herbelin	2014-10-05
*	Classify segfaults as failures in opened bugs.	Xavier Clerc	2014-10-03
*	Classify segfaults as failures in opened bugs	Xavier Clerc	2014-10-03
*	Fixing #3657 (check that both sides of a "change with" have the same	Hugo Herbelin	2014-10-03
*	Test for bug #3652 fixed in 0fb36157b9ba	Hugo Herbelin	2014-10-03
*	Fixing #3623 (unbound evars in types in a call to "change with").	Hugo Herbelin	2014-10-03
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-10-03
*	Adapting output/Arguments_renaming continued.	Hugo Herbelin	2014-10-03
*	Implement module subtyping for polymorphic constants (errors on	Matthieu Sozeau	2014-10-02
*	Fixing bug #2810 (autounfold on local variable declared as hint but cleared).	Hugo Herbelin	2014-10-02
*	An evar name changed in output test.	Hugo Herbelin	2014-10-02
*	Adapting the output test Notations:	Hugo Herbelin	2014-10-02
*	Added make dependency in %.out in output tests.	Hugo Herbelin	2014-10-02
*	Revert "test-suite: New names for vars but the expected invariant is preserved"	Hugo Herbelin	2014-10-02
*	Adapting output/Arguments_renaming.out after fixing printing of	Hugo Herbelin	2014-10-02
*	Updating to the new use of 3 universes, after Hurkens is simplified.	Hugo Herbelin	2014-10-01
*	Removing test for bug #2080.	Pierre-Marie Pédrot	2014-10-01
*	Add a bunch of reproduction files for closed bugs.	Xavier Clerc	2014-09-30
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-30
*	Seeing IntroWildcard as an action intro pattern rather than as a naming pattern	Hugo Herbelin	2014-09-30
*	Restoring non-uniform delta on local and global constants in 2nd order	Hugo Herbelin	2014-09-29
*	Adding a test for bug #2428.	Pierre-Marie Pédrot	2014-09-29
*	Bug fixed.	Matthieu Sozeau	2014-09-29
*	Fix test-suite files	Matthieu Sozeau	2014-09-29
*	In evarconv and unification, expand folded primitive projections to	Matthieu Sozeau	2014-09-29
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	First version of keyed subterm selection in unification.	Matthieu Sozeau	2014-09-27
*	Fix test-suite file.	Matthieu Sozeau	2014-09-27
*	Fix bug #3664 by refolding projections that don't reduce in cbn.	Matthieu Sozeau	2014-09-27
*	Fix semantics of matching with folded/unfolded projections to definitely	Matthieu Sozeau	2014-09-27
*	Fix bug #3672, application of primitive projections as coercions.	Matthieu Sozeau	2014-09-27
*	Fix bug 3662 by actually reducing primitive projections in cbv/compute.	Matthieu Sozeau	2014-09-27
*	Bug fixed.	Matthieu Sozeau	2014-09-27
*	Make pattern_of_constr typed so that we can infer the proper patterns	Matthieu Sozeau	2014-09-27
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
*	Adapting to naming of evars.	Hugo Herbelin	2014-09-27
*	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau	2014-09-26
*	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
*	Adding a test for bug #3653.	Pierre-Marie Pédrot	2014-09-26
*	Test cases for closed bugs.	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
*	Fix bug #3656.	Matthieu Sozeau	2014-09-23
*	Move the specific map_constr_with_binders_left_to_right	Matthieu Sozeau	2014-09-19