coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned	Pierre Letouzey	2014-01-30
*	Mltop: explicitly qualify calls to CUnix	Pierre Letouzey	2014-01-30
*	Load implemented in CoqIDE/STM (closes: #3223)	Enrico Tassi	2014-01-30
*	STM + CoqIDE: stop_worker message and UI	Enrico Tassi	2014-01-30
*	Work around for bug in threads + blocking io streamlined	Enrico Tassi	2014-01-30
*	STM: worker sends back to master the last valid state	Enrico Tassi	2014-01-30
*	STM: tell the user if the master is recomputing states validated by workers	Enrico Tassi	2014-01-30
*	Fixing backtrace handling here and there.	Pierre-Marie Pédrot	2014-01-30
*	-schedule-vi-checking ported to spawn	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
*	-schedule-vi-checking generates better script	Enrico Tassi	2014-01-14
*	STM: fix -async-proofs lazy	Enrico Tassi	2014-01-14
*	Make Require verbose	Pierre Boutillier	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
*	typos	Enrico Tassi	2014-01-07
*	STM: handle side effects of workers correctly	Enrico Tassi	2014-01-06
*	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot	2014-01-06
*	STM: modules do not prevent proofs from being ASync	Enrico Tassi	2014-01-05
*	Proof_using: new syntax + suggestion	Enrico Tassi	2014-01-05
*	Fix coqc -time (Closes: 3201)	Enrico Tassi	2014-01-05
*	STM: fix error messages while in batch mode (closes: 3196)	Enrico Tassi	2014-01-05
*	Paral-ITP: cleanup of command line flags and more conservative default	Enrico Tassi	2014-01-05
*	Fix some warnings with ocamlc 4.01	Enrico Tassi	2014-01-05
*	coqtop: -check-vi-tasks and -schedule-vi-checking	Enrico Tassi	2014-01-05
*	Lemmas: export standard proof terminator	Enrico Tassi	2014-01-04
*	Proof_global: Simpler API for proof_terminator	Enrico Tassi	2014-01-04
*	STM: use sec vars in aux file if no Proof using when building .vi	Enrico Tassi	2014-01-04
*	.vi files: .vo files without proofs	Enrico Tassi	2014-01-04
*	STM: simple refactoring	Enrico Tassi	2014-01-04
*	STM: set loc for aux file when interpreting vernac	Enrico Tassi	2014-01-04
*	STM: record in aux file proof build and check time	Enrico Tassi	2014-01-04
*	Useless Evd.create_evar_defs.	Pierre-Marie Pédrot	2013-12-30
*	STM: capture type checking error (Closes: 3195)	Enrico Tassi	2013-12-24
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	CoqIDE: new feedback "incomplete" to signal partial Qed	Enrico Tassi	2013-12-24
*	cleanup warning	Enrico Tassi	2013-12-24
*	Adding a finer-grained -bt flag to coqtop only triggering backtraces.	Pierre-Marie Pédrot	2013-12-22
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
*	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey	2013-12-16
*	Fix CoqIDE on windows	Enrico Tassi	2013-12-10
*	Fix printing of Ltac's backtrace.	Arnaud Spiwack	2013-12-09
*	Stm: remove an assertion.	Arnaud Spiwack	2013-12-04
*	Fix Admitted.	Arnaud Spiwack	2013-12-04
*	Factoring(continued).	Arnaud Spiwack	2013-12-04
*	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack	2013-12-04