coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Improving printing of "[]" (nil) in spite of the risk of collision	Hugo Herbelin	2014-08-05
*	Testing beautifying on an example.	Hugo Herbelin	2014-08-05
*	Experimentally adding an option for automatically erasing an	Hugo Herbelin	2014-08-05
*	Testing a replacement of "cut" by "enough" on a couple of test files.	Hugo Herbelin	2014-08-05
*	More proofs independent of the names generated by induction/elim over	Hugo Herbelin	2014-08-05
*	Move to a representation of universe polymorphic constants using indices for ...	Matthieu Sozeau	2014-08-03
*	Adding a generalized version of fold_Equal to FMapFacts.	Pierre Courtieu	2014-07-31
*	Simplified rect2, it turns out Arthur's trick was not required.	Maxime Dénès	2014-07-22