coq - The formal proof system

Age	Commit message (Expand)	Author
2014-12-19	Add a backtracking version of Ltac's [match].	Arnaud Spiwack
2014-12-19	When pretyping [uconstr] closures, don't use the local Ltac variable environm...	Arnaud Spiwack
2014-12-19	Fixing performance issue of checker validation.	Pierre-Marie Pédrot
2014-12-19	Fixing checker representation of values.	Pierre-Marie Pédrot
2014-12-19	update md5 sums to make "make check" work	Enrico Tassi
2014-12-19	Fix sigsegv in checker	Enrico Tassi
2014-12-19	Better doc and a few fixes for Proof using.	Enrico Tassi
2014-12-19	Back to the preferred ?n1:=?n2 order of evar-evar unification which got accid...	Hugo Herbelin
2014-12-19	Fixing wrong notation level in #3295.	Hugo Herbelin
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-18	Fixing checker representation of universe lists.	Pierre-Marie Pédrot
2014-12-18	Backporting the change in lists of universes to the checker.	Pierre-Marie Pédrot
2014-12-18	Cleaning up universe list implementation in Univ.	Pierre-Marie Pédrot
2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi
2014-12-18	Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for gram...	mlasson
2014-12-18	Fixed bad newlines in output for std output and emacs.	Pierre Courtieu
2014-12-17	Fix compilation with ocaml 4.0.0	Enrico Tassi
2014-12-17	checker: Change in library on disk values, now using context_sets instead of	Matthieu Sozeau
2014-12-17	Ensuring the good invariants of hashcons table generation in the API.	Pierre-Marie Pédrot
2014-12-17	Fix (actually, properly implement :) hashconsing of projections,	Matthieu Sozeau
2014-12-17	Fixing bug #3796.	Pierre-Marie Pédrot
2014-12-17	Fixing Makefile so that it puts the -thread flag on the right place.	Pierre-Marie Pédrot
2014-12-17	Update checker/values and cic due to changes in case_info and record_body.	Matthieu Sozeau
2014-12-17	Future: blocking by default	Enrico Tassi
2014-12-17	STM: resilient on errors in non delegated proofs	Enrico Tassi
2014-12-17	CoqIDE: cleanup jobs window on worker death	Enrico Tassi
2014-12-17	STM: rename and simplify flags	Enrico Tassi
2014-12-17	STM: simplify state management	Enrico Tassi
2014-12-17	AsyncTaskQueue: simpler model (no parking area, continuation tasks)	Enrico Tassi
2014-12-17	WorkerPool: simpler fuctor and no more parking area	Enrico Tassi
2014-12-17	TQueue: a way to unblock threads begin destroyed waiting on pop	Enrico Tassi
2014-12-17	Spawn: fix request of Gc statistics	Enrico Tassi
2014-12-17	CThread: use a different type for thread friendly in_channels	Enrico Tassi
2014-12-17	Summary: more surgery functions	Enrico Tassi
2014-12-17	Global: export the name of the summary entry	Enrico Tassi
2014-12-17	Dyn: add API to check of two Dyn.t are ==	Enrico Tassi
2014-12-17	Arguments: warn only if no option is given (Close 3860)	Enrico Tassi
2014-12-17	CoqIDE: better messages	Enrico Tassi
2014-12-17	Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must hav...	Pierre Boutillier
2014-12-16	#3828 is solved.	Hugo Herbelin
2014-12-16	Moving #2447 (congruence) to fixed.	Hugo Herbelin
2014-12-16	In CHANGES, alerting about stronger check on notation level modifiers.	Hugo Herbelin
2014-12-16	More printers for ltac signatures.	Hugo Herbelin
2014-12-16	Test for #3654.	Hugo Herbelin
2014-12-16	fix bug #2447 in congruence	Pierre Corbineau
2014-12-16	fix bug #2447 in congruence	Pierre Corbineau
2014-12-16	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot