coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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