coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	fix simple test for paral-itp	Enrico Tassi	2014-01-06
*	fix typo	Enrico Tassi	2014-01-06
*	STM: handle side effects of workers correctly	Enrico Tassi	2014-01-06
*	STM: fix worker crash when doing vm_compute	Enrico Tassi	2014-01-06
*	Algebraized "No such hypothesis" errors	Pierre-Marie Pédrot	2014-01-06
*	Add a test suite file for Ltac's "+" tactical.	Arnaud Spiwack	2014-01-06
*	Revert "Rewriting the proof monad mechanism. Now it uses pure OCaml code, wit...	Arnaud Spiwack	2014-01-06
*	refman: fist stab at Asynchronous Proofs	Enrico Tassi	2014-01-05
*	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
*	nanoPG: compete rewriting with more Emacs/PG like features	Enrico Tassi	2014-01-05
*	Disable GlobRef feedback (CoqIDE does nothing with them)	Enrico Tassi	2014-01-05
*	Environ: export API to transitively close a set of section variables	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
*	Future: allow custom action when a delegated future is forced	Enrico Tassi	2014-01-04
*	kernel: save in aux the list of section variables used	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
*	Aux_file: cache information at compile time for later (re)use	Enrico Tassi	2014-01-04
*	Remove obsolete comment about Let being processed synchronously	Enrico Tassi	2014-01-04
*	Code cleaning in Rewrite, may also result faster.	Pierre-Marie Pédrot	2014-01-04
*	Reference the 'external' tactic.	Guillaume Melquiond	2014-01-01
*	When resetting an evarmap with the unsafe function Evd.evars_reset_evd with	Pierre-Marie Pédrot	2013-12-30
*	Useless Evd.create_evar_defs.	Pierre-Marie Pédrot	2013-12-30
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Avoid generating .ml files in native compiler.	Maxime Dénès	2013-12-29
*	Got rid of unused lazy flag in the native compiler.	Maxime Dénès	2013-12-29
*	Revert "Partial revert of r16711"	Maxime Dénès	2013-12-28
*	Removing native_name reference from constant_body.	Maxime Dénès	2013-12-28
*	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
*	Future: optional greedy chaining	Enrico Tassi	2013-12-24
*	cleanup warning	Enrico Tassi	2013-12-24