coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Adding a "time" tactical for benchmarking purposes. In case the tactic	Hugo Herbelin	2014-07-13
*	An outdated comment + comment layout.	Arnaud Spiwack	2014-07-11
*	STM: let toploop plugins specify the flags for STM workers	Enrico Tassi	2014-07-11
*	STM: flag to turn off branch reopening	Enrico Tassi	2014-07-11
*	Feedback: LoadedFile + Goals	Enrico Tassi	2014-07-11
*	make the standard logging facility stm aware	Enrico Tassi	2014-07-11
*	option to always delegate futures to workers	Enrico Tassi	2014-07-10
*	more APIs in TQueue and CThread	Enrico Tassi	2014-07-10
*	check_for_interrupt: better (but slower) in threading mode	Enrico Tassi	2014-07-10
*	Revert "time tac" (committed by mistake).	Hugo Herbelin	2014-07-07
*	time tac	Hugo Herbelin	2014-07-07
*	Adding a coiterator to IStream.	Pierre-Marie Pédrot	2014-07-03
*	all coqide specific files moved into ide/	Enrico Tassi	2014-06-25
*	Less ocaml warnings.	Hugo Herbelin	2014-06-21
*	Deprecate useless option -quality.	Guillaume Melquiond	2014-06-13
*	Deprecate useless option -unsafe.	Guillaume Melquiond	2014-06-13
*	Deprecate options -dont, -lazy, -force-load-proofs.	Guillaume Melquiond	2014-06-13
*	Compute the trace of a universe inconsistency only when explicitly required	Pierre-Marie Pédrot	2014-06-10
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	Timeout implementation for Windows based on threads.	Pierre-Marie Pédrot	2014-06-08
*	Enforce a correct exception handling in declaration_hooks	Enrico Tassi	2014-06-08
*	Moving a Thread.yield in check_interrupt.	Pierre-Marie Pédrot	2014-06-07
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	Declare: fix Future management	Enrico Tassi	2014-05-16
*	Future: better error message	Enrico Tassi	2014-05-15
*	Moving Dnet-related code to tactics/.	Pierre-Marie Pédrot	2014-05-08
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Fixing ml-doc.	Pierre-Marie Pédrot	2014-05-01
*	Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to	Hugo Herbelin	2014-04-28
*	Adding a stm/ folder, as asked during last workgroup. It was essentially moving	Pierre-Marie Pédrot	2014-04-25
*	Future: memory optimization when forcing a chained pure computation	Enrico Tassi	2014-04-25
*	Adding a debug printer for futures.	Pierre-Marie Pédrot	2014-04-25
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Have the feedback bus as a backend for dumping globs.	Carst Tankink	2014-04-10
*	Removing handshake from Spawn. It used marshalling, which is bad for	Pierre-Marie Pédrot	2014-04-09
*	Change handling of loadpath and mlpath.	Guillaume Melquiond	2014-04-06
*	Slightly more efficient Array.smartmap & related.	Pierre-Marie Pédrot	2014-03-20
*	Stateid: export a Set module	Enrico Tassi	2014-03-13
*	STM: move out a couple of submodules	Enrico Tassi	2014-03-13
*	Stm: smarter delegation policy	Enrico Tassi	2014-03-12
*	Uses slashes for install and config directories	Virgile Prevosto	2014-03-06
*	Canary testing absence of generic equality for KerNames	Pierre-Marie Pédrot	2014-03-05
*	Adding a canary library. This canary is imperfect. It allows serialization	Pierre-Marie Pédrot	2014-03-05
*	Fixing compilation on OCaml 4.01.	Pierre-Marie Pédrot	2014-03-05
*	Fixing previous commit. Forgot to include some code.	Pierre-Marie Pédrot	2014-03-05
*	Added a new module HMap. It works (almost) like Map, except that it expects	Pierre-Marie Pédrot	2014-03-05
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Adding a CSet module in Coq lib.	Pierre-Marie Pédrot	2014-03-05
*	Replacing arguments of Trie by a cancellable monoid.	Pierre-Marie Pédrot	2014-03-03