coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
*	Fixing #3641 (loop in e_contextually, introduced in r16525).	Hugo Herbelin	2014-09-19
*	Fix constrMatching as well as change/e_contextually to allow	Matthieu Sozeau	2014-09-18
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier	2014-09-18
*	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau	2014-09-17
*	Fix bug #3633 properly, by delaying the interpetation of constrs in	Matthieu Sozeau	2014-09-17
*	Revert "While resolving typeclass evars in clenv, touch only the ones that ap...	Matthieu Sozeau	2014-09-17
*	While resolving typeclass evars in clenv, touch only the ones that appear in the	Matthieu Sozeau	2014-09-17
*	Update test-suite files after last commit. Add a file for rewrite_strat	Matthieu Sozeau	2014-09-17
*	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau	2014-09-17
*	Undo prints only if coqtop \|\| emacs	Enrico Tassi	2014-09-16
*	fix test-suite/success/decl_mode.v	Enrico Tassi	2014-09-16
*	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau	2014-09-15