coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	For type classes, tell that VarInstance's behave like GoalEvar (avoid a loop ...	Hugo Herbelin	2014-09-18
*	mltop: when a plugin is loaded store its full path in the summary	Enrico Tassi	2014-09-18
*	Reductionops: (Co)Fixpoints are always refolded during iota	Pierre Boutillier	2014-09-18
*	fix coq_makefile	Pierre Boutillier	2014-09-18
*	configure.ml: opam camlp5 + system ocaml works	Pierre Boutillier	2014-09-18
*	seems to fix a looping coq-tex (when compiled with camlp4)	Pierre Boutillier	2014-09-18
*	Be more conservative and keep the use of eq_constr in pretyping/ functions.	Matthieu Sozeau	2014-09-17
*	Fix bug #3593, making constr_eq and progress work up to	Matthieu Sozeau	2014-09-17
*	Fix bug #3633 properly, by delaying the interpetation of constrs in	Matthieu Sozeau	2014-09-17
*	Change some Defined into Qed.	Guillaume Melquiond	2014-09-17
*	Add some missing Proof statements.	Guillaume Melquiond	2014-09-17
*	Remove pointless regex for '""' as the empty string already matches it.	Guillaume Melquiond	2014-09-17
*	Revert "coqc: execvp is now available even on win32"	Enrico Tassi	2014-09-17
*	win32: remove outdated splash screen	Enrico Tassi	2014-09-17
*	Fix highlighting of "Hint Unfold" and "Hint Rewrite".	Guillaume Melquiond	2014-09-17