coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Changed implementation of lib/heap.ml to use Braun trees	Jean-Christophe Filliatre	2014-10-25
*	-help failing (fix 3762)	Enrico Tassi	2014-10-24
*	Monad: change the error managing of two-list combinators.	Arnaud Spiwack	2014-10-23
*	Goal printing made uniform: always done in STM (close 3585)	Enrico Tassi	2014-10-22
*	An additional [List.iter] monadic combinator.	Arnaud Spiwack	2014-10-22
*	Add more primitives to the [Monad.Make] arguments.	Arnaud Spiwack	2014-10-22
*	Proofview: move [list_goto] to the [CList] module.	Arnaud Spiwack	2014-10-22
*	Add a two-list monadic fold_left iterator.	Arnaud Spiwack	2014-10-22
*	Small optimisation in the monadic list combinators.	Arnaud Spiwack	2014-10-22
*	Factor module signatures.	Arnaud Spiwack	2014-10-22
*	When loading libraries, feed back dependencies.	Carst Tankink	2014-10-13
*	STM: primitives to snapshot a .vi while in interactive mode	Enrico Tassi	2014-10-13
*	library/opaqueTables: enable their use in interactive mode	Enrico Tassi	2014-10-13
*	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