coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
*	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau	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
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-26
*	Add missing "Fail" to bug cases.	Xavier Clerc	2014-09-26
*	Bug #3566 is fixed.	Xavier Clerc	2014-09-26
*	Adding a test for bug #3653.	Pierre-Marie Pédrot	2014-09-26
*	Test cases for closed bugs.	Xavier Clerc	2014-09-26
*	Fix incorrect assert false in detyping.	Matthieu Sozeau	2014-09-25
*	Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",	Xavier Clerc	2014-09-25
*	Add several reproduction files for bugs.	Xavier Clerc	2014-09-25
*	Improve consistency of whitespace (beautifier).	Xavier Clerc	2014-09-25
*	Remove some 'deprecated' warnings.	Xavier Clerc	2014-09-25
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25
*	Update test-suite files.	Matthieu Sozeau	2014-09-24
*	Rename eq_constr functions in Evd to not break backward compatibility	Matthieu Sozeau	2014-09-24
*	Return a Prop not an arbitrary Type, and correct a typo.	Matthieu Sozeau	2014-09-24
*	Make eq_pattern_test/eq_test work up to the equivalence of primitive	Matthieu Sozeau	2014-09-24
*	Using an or_var rather than the hack with loc for coding a pure ident	Hugo Herbelin	2014-09-24
*	Added support for interpreting hyp lists in tactic notations.	Hugo Herbelin	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
*	Make the retroknowledge marshalable.	Arnaud Spiwack	2014-09-24
*	Fix a message.	Arnaud Spiwack	2014-09-24
*	coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".	Arnaud Spiwack	2014-09-24
*	Fix bug #3656.	Matthieu Sozeau	2014-09-23
*	ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite	Matthieu Sozeau	2014-09-23
*	Fix bug in setoid_rewrite introduced by PMP's commits, which was creating	Matthieu Sozeau	2014-09-23
*	adds general facts in the Reals library, whose need was detected in	Yves Bertot	2014-09-23
*	Correction of error message (bug 3359)	Julien Forest	2014-09-22
*	Fixing bug 3951	Julien Forest	2014-09-22
*	Rewrite.apply_lemma is written in state passing style.	Pierre-Marie Pédrot	2014-09-21
*	More invariants in the code of Refine.	Pierre-Marie Pédrot	2014-09-21
*	Removing a nonsensical Errors.push.	Pierre-Marie Pédrot	2014-09-21
*	Move the specific map_constr_with_binders_left_to_right	Matthieu Sozeau	2014-09-19
*	Fixes in Ltac pattern-matching on primitive projections	Matthieu Sozeau	2014-09-19
*	Use smart mapping in map_constr_with_binders_left_to_right.	Matthieu Sozeau	2014-09-19
*	Fixing bug #3646.	Pierre-Marie Pédrot	2014-09-19
*	win32: embed NSIS for plugin writers	Enrico Tassi	2014-09-19
*	Fixing #3641 (loop in e_contextually, introduced in r16525).	Hugo Herbelin	2014-09-19
*	Revert change of e_contextually as it needlessly expands all primitive	Matthieu Sozeau	2014-09-19
*	Fix constrMatching as well as change/e_contextually to allow	Matthieu Sozeau	2014-09-18
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Do not try to match on a subterm that is not closed in find_subterm.	Matthieu Sozeau	2014-09-18
*	Clean a bit of univ.ml, add credits.	Matthieu Sozeau	2014-09-18
*	Fixing strange evarmap leak in goals.	Pierre-Marie Pédrot	2014-09-18