coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	-schedule-vi-checking ported to spawn	Enrico Tassi	2014-01-26
*	CoqIDE: command line for extra coqtop "flags"	Enrico Tassi	2014-01-26
*	break > 80 cols line	Enrico Tassi	2014-01-26
*	STM: ported to spawn	Enrico Tassi	2014-01-26
*	CoqIDE: ported to spawn	Enrico Tassi	2014-01-26
*	Spawn: managed processes	Enrico Tassi	2014-01-26
*	configure.ml fixed wrt Win32 + byte-only + coqide	Enrico Tassi	2014-01-26
*	Adding a test for bug #3023.	Pierre-Marie Pédrot	2014-01-25
*	More in CHANGES.	Pierre-Marie Pédrot	2014-01-25
*	[Coercion]s use [Sortclass], not [Prop] (in docs)	Jason Gross	2014-01-24
*	The configure script now outputs the parameters it was fed with in	Pierre-Marie Pédrot	2014-01-24
*	bug correction in proving principles of function	jforest	2014-01-20
*	Using full paths in coqdep -dumpgraph.	Pierre-Marie Pédrot	2014-01-19
*	Fixing coqdep graph printing. The transitive reduction algorithm was bugged.	Pierre-Marie Pédrot	2014-01-19
*	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot	2014-01-19
*	Fixing an interpretation bug with tactics in notations. For some obscure	Pierre-Marie Pédrot	2014-01-19
*	Fixing checker compilation, which was broken by the following commit:	Pierre-Marie Pédrot	2014-01-19
*	Relaxing the sort elimination check to allow for let-bindings in arities.	Maxime Dénès	2014-01-18
*	Makefiles use $(foo), not $foo, for variables	Jason Gross	2014-01-18
*	Fixup make clean and .merlin	Pierre Boutillier	2014-01-18
*	Follow-up of bugfix for #3204: local definitions were not handled properly.	Pierre-Marie Pédrot	2014-01-17
*	Fixing bug #1758: Print Hint output can be misleading if variable shadows hyp...	Pierre-Marie Pédrot	2014-01-17
*	Update .mailmap with recent contributors.	Arnaud Spiwack	2014-01-17
*	Fixing bugs #1039: Hypotheses don't respect Barendregt convention	Pierre-Marie Pédrot	2014-01-16
*	Implementing transitive reduction in the dependency graph printing	Pierre-Marie Pédrot	2014-01-16
*	Christmas is over...	Maxime Dénès	2014-01-15
*	Test case containing a proof of false due to a DeBruijn off-by-one error in the	Maxime Dénès	2014-01-15
*	-schedule-vi-checking generates better script	Enrico Tassi	2014-01-14
*	STM: fix -async-proofs lazy	Enrico Tassi	2014-01-14
*	Removing unused tactics in rewrite.	Pierre-Marie Pédrot	2014-01-14
*	Make Require verbose	Pierre Boutillier	2014-01-13
*	rename Paral-ITP demo file	Enrico Tassi	2014-01-13
*	Paral-ITP demo: better comments	Enrico Tassi	2014-01-13
*	STM: fix very simple demo	Enrico Tassi	2014-01-13
*	Declared ML Module are not uncapitalized/capitalized/uncapitalized/...	Pierre Boutillier	2014-01-13
*	Fixing typo in reference manual from previous commit	Hugo Herbelin	2014-01-13
*	Documenting old but useful command "Print Tables".	Hugo Herbelin	2014-01-13
*	'Pretty' printer for wf_paths	Pierre	2014-01-11
*	Fixing bug #3144.	Pierre-Marie Pédrot	2014-01-10
*	Useless Array.of_list	Pierre-Marie Pédrot	2014-01-10
*	Omega: avoiding distinct proof-terms on repeated identical runs	Pierre Letouzey	2014-01-10
*	Exporting the full pretyper options in Goal.constr_of_raw.	Pierre-Marie Pédrot	2014-01-10
*	Fix bug#2080: error message on Ltac name clash with primitive tactics	xclerc	2014-01-10
*	Goodbye typerex, Hello merlin	Pierre	2014-01-09
*	md5 for MacOS	Pierre	2014-01-09
*	Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd	Pierre Letouzey	2014-01-08
*	typos	Enrico Tassi	2014-01-07
*	STM: additional fix for STM + vm_compute	Enrico Tassi	2014-01-07
*	Adding a -dumpgraph option to Coqdep that output the graph dependency of the	Pierre-Marie Pédrot	2014-01-06
*	CoqIDE: do not unfocus if not needed on errors (closes: 3197)	Enrico Tassi	2014-01-06