coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	A version of Fin.rect2 that is compatible with the fix of the guard condition.	Maxime Dénès	2014-07-22
*	Fixed proof of irrelevance of le on nat, inspired by the	Maxime Dénès	2014-07-22
*	Completing c236b51348d2 by fixing EqdepFactsv actually committing the	Hugo Herbelin	2014-07-17
*	Added a (constructive) proof of Weak Konig's lemma for decidable trees.	Hugo Herbelin	2014-07-15
*	Some basics facts about eq_dep.	Hugo Herbelin	2014-07-15
*	MSetRBT: unfortunate typo in compare_height (fix #3413)	Pierre Letouzey	2014-07-10
*	Arith: full integration of the "Numbers" modular framework	Pierre Letouzey	2014-07-09
*	Fixing bug #3270. Patch by Robbert Krebbers.	Pierre-Marie Pédrot	2014-07-08
*	Move Params definition in generalize rewriting out of a section so that	Matthieu Sozeau	2014-06-29
*	Avoid using a deprecated lemma in the standard library.	Guillaume Melquiond	2014-06-26
*	Remove some theories that have been deprecated for 10 years.	Guillaume Melquiond	2014-06-26
*	Export the right modules in Setoid, avoiding anomalies in generalized rewriting.	Matthieu Sozeau	2014-06-26
*	Deactivate the "Standard Propositions Naming" flag, source of a lot of	Hugo Herbelin	2014-06-26
*	Cleanup treatment of template universe polymorphism (thanks to E. Tassi	Matthieu Sozeau	2014-06-20
*	Make standard library independent of the names generated by	Hugo Herbelin	2014-06-04