coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fixup leading ./ path cleaning	Pierre Boutillier	2014-10-09
*	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin	2014-10-07
*	A few improvements on pattern-matching compilation.	Hugo Herbelin	2014-10-05
*	STM: report the (structured) goals as XML	Carst Tankink	2014-10-01
*	Remove some 'deprecated' warnings.	Xavier Clerc	2014-09-25
*	Fix debug printing with primitive projections.	Matthieu Sozeau	2014-09-18
*	Undo prints only if coqtop \|\| emacs	Enrico Tassi	2014-09-16
*	Undo: if the ui is coqtop (command line) then Undo is not part of the doc.	Enrico Tassi	2014-09-09
*	toploop plugins taken into account when printing --help (close: 3535)	Enrico Tassi	2014-09-09
*	Removing dead code relative to the XML plugin.	Pierre-Marie Pédrot	2014-09-08
*	Adding a Ftactic module for potentially focussing tactics.	Pierre-Marie Pédrot	2014-09-05
*	coqworkmgr	Enrico Tassi	2014-09-02
*	Type-safe version of genarg list / pair / opt functions.	Pierre-Marie Pédrot	2014-08-29
*	Simplification of Genarg unpackers.	Pierre-Marie Pédrot	2014-08-29
*	Fixing bug #3541.	Pierre-Marie Pédrot	2014-08-28
*	"allows to", like "allowing to", is improper	Jason Gross	2014-08-25
*	STM: new "par:" goal selector, like "all:" but in parallel	Enrico Tassi	2014-08-05
*	STM: code restructured to reuse task queue for tactics	Enrico Tassi	2014-08-05
*	STM: encapsulate Pp.message in Feedback.feedback	Carst Tankink	2014-08-04
*	Removing the call to Weak.get_copy in hashsets.	Pierre-Marie Pédrot	2014-07-31
*	Improve intersection of regular trees.	Maxime Dénès	2014-07-31
*	Pp: only one default feedback id	Enrico Tassi	2014-07-29
*	Pp compiles after feedback	Enrico Tassi	2014-07-29
*	Revert "Adding a "is_val" primitive to IStream."	Pierre-Marie Pédrot	2014-07-24
*	Refine check_is_subterm.	Maxime Dénès	2014-07-22
*	Made intersection on regular trees less intensional.	Maxime Dénès	2014-07-22
*	Refining match subterm and commutative cut rules. The parameters that are	Maxime Dénès	2014-07-22
*	Adding a "is_val" primitive to IStream.	Pierre-Marie Pédrot	2014-07-22
*	Universe level maps use HMaps.	Pierre-Marie Pédrot	2014-07-21
*	Missing primitives in HMap.	Pierre-Marie Pédrot	2014-07-21
*	Fixing semantics of HSet.inter and HSet.diff.	Pierre-Marie Pédrot	2014-07-21
*	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