coq - The formal proof system

Age	Commit message (Expand)	Author
2016-11-24	Fix some documentation typos.	Guillaume Melquiond
2016-10-12	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot
2016-10-03	Remove if_then_else. Use tryif instead.	Théo Zimmermann
2016-07-07	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot
2016-07-05	Move option_map notation up	Jason Gross
2016-07-05	Restore option_map in FMapFacts	Jason Gross
2016-06-18	Giving a more natural semantics to injection by default.	Hugo Herbelin
2015-12-07	Fix some typos.	Guillaume Melquiond
2014-12-25	Forbid Require inside interactive modules and module types.	Maxime Dénès
2014-10-01	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier
2014-09-27	Keyed unification option, compiling the whole standard library	Matthieu Sozeau
2014-09-09	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau
2014-08-25	instanciation is French, instantiation is English	Jason Gross
2014-08-25	Grammar: "allowing to" is not proper English	Jason Gross
2014-08-05	More proofs independent of the names generated by induction/elim over	Hugo Herbelin
2014-07-31	Adding a generalized version of fold_Equal to FMapFacts.	Pierre Courtieu
2014-06-26	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond
2014-06-20	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau
2014-06-04	Make standard library independent of the names generated by	Hugo Herbelin
2014-06-01	Making those proofs which depend on names generated for the arguments	Hugo Herbelin
2014-05-06	Fix after merge.	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-05-02	Cbn is happier when ?SetPositive fixpoints have the set as recursive argument	Pierre Boutillier
2014-05-02	Eta contractions to please cbn	Pierre Boutillier
2013-07-17	"Boolean Equality" and "Case Analysis" are already off by default...	letouzey
2013-01-18	Unset Asymmetric Patterns	pboutill
2012-12-18	No more constant named "int" in Coq theories (cf bug #2878)	letouzey
2012-10-01	Ltac repeat is in fact already doing progress	letouzey
2012-07-05	Kills the useless tactic annotations "in \|- *"	letouzey
2012-07-05	Open Local Scope ---> Local Open Scope, same with Notation and alii	letouzey
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-05-15	Intuition: temporary(?) restore the unconditional unfolding of not	letouzey
2012-04-15	Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680).	herbelin
2012-03-14	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau
2012-01-31	Revert "Tentative to fix bug #2628 by not letting intuition break records. Mi...	msozeau
2012-01-28	Tentative to fix bug #2628 by not letting intuition break records. Might be t...	msozeau
2011-11-21	theories/, plugins/ and test-suite/ ported to the Arguments vernacular	gareuselesinge
2011-10-14	MSet/FSet/FMap : add more explicitly an alternative spec for fold via fold_right	letouzey
2011-10-07	fsetdec : non-atomic elements are now transformed as variables first (fix #2464)	letouzey
2011-10-07	Improved handling of element equalities in fsetdec (fix #2467)	letouzey
2011-05-05	Modularization of BinInt, related fixes in the stdlib	letouzey
2011-03-13	- Add modulo_delta_types flag for unification to allow full	msozeau
2011-02-17	- Use transparency information all the way through unification and	msozeau
2011-02-16	Fix compilation issues.	msozeau
2011-02-14	- Fix treatment of globality flag for typeclass instance hints (they	msozeau
2011-01-06	s/appartness/membership/g (Closes: #2470)	glondu
2010-12-17	Cosmetic : let's take advantage of the n-ary exists notation	letouzey
2010-10-22	FMapFacts: typo noticed by Aaron	letouzey
2010-09-20	Extraction: re-introduce some eta-expansions in rare situations leading to '_...	letouzey
2010-09-17	For the moment, two small manual eta-expansions to avoid '_a after extraction	letouzey