coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Failing on unbound notation variable in notation level modifiers	Hugo Herbelin	2014-12-15
*	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-11
*	Added an arithmetical characterization of the hypothesis of WKL.	Hugo Herbelin	2014-12-01
*	Clarifying the role of ListSet.v in the library, compared to other	Hugo Herbelin	2014-11-18
*	Enforcing a stronger difference between the two syntaxes "simpl	Hugo Herbelin	2014-11-16
*	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-11-02
*	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-27
*	EqdepFacts: generalize statements which were wrongly restricted to Prop.	Arnaud Spiwack	2014-10-22
*	Fixing typo absorption (bug #3751).	Hugo Herbelin	2014-10-22
*	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-17
*	ConstructiveEpsilon: simplify the before_witness type using non-uniform param...	Arnaud Spiwack	2014-10-16
*	Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name	Matthieu Sozeau	2014-10-11
*	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-10
*	eta contractions	Pierre Boutillier	2014-10-01
*	argument flip of Cyclic31.nshiftr and Cyclic31.nshiftl	Pierre Boutillier	2014-10-01
*	Simpl less (so that cbn will not simpl too much)	Pierre Boutillier	2014-10-01
*	Keyed unification option, compiling the whole standard library	Matthieu Sozeau	2014-09-27
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
*	ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...	Arnaud Spiwack	2014-09-26
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: fix coqdoc formatting in a comment.	Arnaud Spiwack	2014-09-26
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25
*	Return a Prop not an arbitrary Type, and correct a typo.	Matthieu Sozeau	2014-09-24
*	Hurkens.v: show proofs in coqdoc.	Arnaud Spiwack	2014-09-24
*	Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].	Arnaud Spiwack	2014-09-24
*	Hurkens.v: coqdoc documentation.	Arnaud Spiwack	2014-09-24
*	A new version of Hurkens.v.	Arnaud Spiwack	2014-09-24
*	adds general facts in the Reals library, whose need was detected in	Yves Bertot	2014-09-23
*	Change some Defined into Qed.	Guillaume Melquiond	2014-09-17
*	Add some missing Proof statements.	Guillaume Melquiond	2014-09-17
*	Change an axiom into a definition.	Guillaume Melquiond	2014-09-17
*	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau	2014-09-09
*	Removing the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Prove forall extensionality	Jason Gross	2014-08-26
*	sed s'/_one_var/_on/g'	Jason Gross	2014-08-26
*	Generalize EqdepFacts	Jason Gross	2014-08-26
*	"allows to", like "allowing to", is improper	Jason Gross	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-25
*	Adding a new intro-pattern for "apply in" on the fly. Using syntax	Hugo Herbelin	2014-08-18
*	Factorizing cutrewrite (to be made obsolote) and dependent rewrite (to	Hugo Herbelin	2014-08-18
*	A couple of fixes/improvements in -beautify, but backtracking on	Hugo Herbelin	2014-08-12
*	Instead of relying on a trick to make the constructor tactic parse, put	Pierre-Marie Pédrot	2014-08-07
*	Removing the "constructor" tactic from the AST.	Pierre-Marie Pédrot	2014-08-07