coq - The formal proof system

Age	Commit message (Expand)	Author
2015-03-04	Introducing MMaps, a modernized FMaps.	Pierre Letouzey
2015-03-04	Introducing MMaps, a modernized FMaps.	Pierre Letouzey
2015-02-26	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-26	Revert "Fixing bug #4035 (support for dependent destruction within ltac code)."	Maxime Dénès
2015-02-25	Reorder the steps of the easy tactic. (Fix for bug #2630)	Guillaume Melquiond
2015-02-23	Merge branch 'v8.5' into trunk	Enrico Tassi
2015-02-23	Fix some typos in comments.	Guillaume Melquiond
2015-02-18	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-16	Fixing bug #4035 (support for dependent destruction within ltac code).	Hugo Herbelin
2015-02-15	Merge branch 'v8.5'	Pierre-Marie Pédrot
2015-02-14	dependent destruction: Fix (part of) bug #3961, by fixing dependent *	Matthieu Sozeau
2015-01-18	Merge branch '8.5' into trunk	Matthieu Sozeau
2015-01-18	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau
2015-01-18	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau
2015-01-18	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau
2015-01-18	There was one more universe needed due to the use of now non-universe-polymor...	Matthieu Sozeau
2015-01-16	Add two lemmas about firstn to the List standard library.	Sébastien Hinderer
2015-01-16	Lemmas related to the firstn function over lists.	Sébastien Hinderer
2015-01-16	ListSet: follow-up of Sebastien's last commit	Pierre Letouzey
2015-01-16	Work in progress on listset.	Sébastien Hinderer
2015-01-15	Correct restriction of vm_compute when handling universe polymorphic	Matthieu Sozeau
2015-01-15	Remove typeclass opaque directive, some proofs in the stdlib rely on it being...	Matthieu Sozeau
2015-01-15	Optionally allow eta-conversion during unification for type classes.	Matthieu Sozeau
2015-01-12	Update headers.	Maxime Dénès
2014-12-28	Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...	Arnaud Spiwack
2014-12-25	Forbid Require inside interactive modules and module types.	Maxime Dénès
2014-12-18	Adds two lemmas about hderror to the List standard library.	Sébastien Hinderer
2014-12-18	Implement the nodup function on lists and prove associated results.	Sébastien Hinderer
2014-12-18	Lists: enhanced version of Seb's last commit on Exists/Forall	Pierre Letouzey
2014-12-18	Lists: a few results on Exists and Forall and a bit of code cleanup.	Sébastien Hinderer
2014-12-15	Failing on unbound notation variable in notation level modifiers	Hugo Herbelin
2014-12-11	List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)	Pierre Letouzey
2014-12-11	First series of results on lists.	Sébastien Hinderer
2014-12-01	Added an arithmetical characterization of the hypothesis of WKL.	Hugo Herbelin
2014-11-18	Clarifying the role of ListSet.v in the library, compared to other	Hugo Herbelin
2014-11-16	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin
2014-11-02	Improving elimination with indices, getting rid of intrusive residual	Hugo Herbelin
2014-11-02	Supporting "at occs" as a short-hand for "in \|- * at occs" in "destruct".	Hugo Herbelin
2014-10-27	Make sure that Logic/ExtensionalityFacts gets compiled.	Guillaume Melquiond
2014-10-27	Fix some typos.	Guillaume Melquiond
2014-10-27	Fix some typos in comments.	Guillaume Melquiond
2014-10-22	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack
2014-10-22	Fixing typo absorption (bug #3751).	Hugo Herbelin
2014-10-17	Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...	Hugo Herbelin
2014-10-17	Essai où assert_style n'est utilisé que si pas visuellement une équation;	Hugo Herbelin
2014-10-16	ConstructiveEpsilon: simplify the before_witness type using non-uniform param...	Arnaud Spiwack
2014-10-11	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau
2014-10-10	Give the same argument name for the record binder of type class	Matthieu Sozeau
2014-10-10	Fix segfault in native compiler on int31 division.	Maxime Dénès
2014-10-01	eta contractions	Pierre Boutillier