coq - The formal proof system

Age	Commit message (Expand)	Author
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
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-09-27	Keyed unification option, compiling the whole standard library	Matthieu Sozeau
2014-09-26	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-25	Hurkens.v: update comments.	Arnaud Spiwack
2014-09-24	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-23	adds general facts in the Reals library, whose need was detected in	Yves Bertot
2014-09-17	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-09	- Fix printing and parsing of primitive projections, including the Set	Matthieu Sozeau
2014-09-08	Removing the XML plugin.	Pierre-Marie Pédrot
2014-08-26	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-25	"allows to", like "allowing to", is improper	Jason Gross
2014-08-25	instanciation is French, instantiation is English	Jason Gross