coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Proof using: do not clear letins (unless they use a cleared var)	Enrico Tassi	2014-12-29
*	Use [Proof using] to make sure that [List.in_flat_map] doesn't grab too many ...	Arnaud Spiwack	2014-12-28
*	Call nf_constraints also when compiling directly to vo	Enrico Tassi	2014-12-28
*	Proof using: call "clear" to remove from sight the vars not selected	Enrico Tassi	2014-12-28
*	remove debug prints (leftover)	Enrico Tassi	2014-12-28
*	STM: check with the kernel proof terms on the worker too	Enrico Tassi	2014-12-27
*	STM: fix processing of errors	Enrico Tassi	2014-12-27
*	STM: module Pp is open	Enrico Tassi	2014-12-27
*	proof_global: make it possible to call close_proof in a worker	Enrico Tassi	2014-12-27
*	include test-suite/coqchk in the summary log	Enrico Tassi	2014-12-27
*	universes_of_constant: do a proper set union of body and type univs	Enrico Tassi	2014-12-27
*	Revert "Term: include a function to print terms"	Enrico Tassi	2014-12-27
*	new test for coqchk	Enrico Tassi	2014-12-26
*	coqchk: flush the pp buffer from time to time	Enrico Tassi	2014-12-26
*	STM: do not call process_error twice (Close: 3880)	Enrico Tassi	2014-12-26
*	Call Evd.nf_constraints only on Univ Poly constants	Enrico Tassi	2014-12-26
*	STM: remove dead code	Enrico Tassi	2014-12-26
*	Term: include a function to print terms	Enrico Tassi	2014-12-26
*	Document 6d5b56d971 (forbid Require inside modules).	Maxime Dénès	2014-12-25
*	Forbid Require inside interactive modules and module types.	Maxime Dénès	2014-12-25
*	Inlining Spawn.kill_if in the one place were it was actually used, thus	Pierre-Marie Pédrot	2014-12-25
*	STM: cleanup code for Admitted	Enrico Tassi	2014-12-23
*	Vi2vo: fix handling of univ constraints coming from the body	Enrico Tassi	2014-12-23
*	Minor modification of CHANGE.	Pierre Courtieu	2014-12-23
*	A global [gfail] tactic which works like [fail] except that it fails even if ...	Arnaud Spiwack	2014-12-23
*	Remove compatibility layer from Ltac's [fail].	Arnaud Spiwack	2014-12-23
*	Fix compilation error in some configurations.	Arnaud Spiwack	2014-12-23
*	Dead code in Univ.	Pierre-Marie Pédrot	2014-12-21
*	Win32: fix installer	Enrico Tassi	2014-12-19
*	Install .v and .glob files too	Enrico Tassi	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-19
*	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-18
*	Fix compilation with ocaml 4.0.0	Enrico Tassi	2014-12-17