coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Complete a truncated comment	Arnaud Spiwack	2016-11-08
\| \| \| \| \|	Introduce by myself, I'm afraid, in #308. Noticed by PMP during the review, but I forgot to fix it before merge.
*	Fix #4416: - Incorrect "Error: Incorrect number of goals"	Arnaud Spiwack	2016-10-10
\| \| \| \| \| \| \| \|	In `Ftactic` the number of results could desynchronise with the number of goals when some goals were solved by side effect in a different branch of a `DISPATCH`. See [coq-bugs#4416](https://coq.inria.fr/bugs/show_bug.cgi?id=4416).
*	Monad: change the error managing of two-list combinators.	Arnaud Spiwack	2014-10-23
\| \| \|	Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
*	An additional [List.iter] monadic combinator.	Arnaud Spiwack	2014-10-22
\|
*	Add more primitives to the [Monad.Make] arguments.	Arnaud Spiwack	2014-10-22
\| \| \| \|	For optimisation purposes.
*	Add a two-list monadic fold_left iterator.	Arnaud Spiwack	2014-10-22
\|
*	Adding a Ftactic module for potentially focussing tactics.	Pierre-Marie Pédrot	2014-09-05
\| \| \| \| \| \|	The code for the module was moved from Tacinterp. We still expose partially the implementation of the Ftactic.t type, for the sake of simplicity. It may be dangerous if used improperly though.
*	Tacinterp: more refactoring.	Arnaud Spiwack	2014-02-27
\| \| \|	Introducing List.fold_right and List.fold_left in Monad.
*	Tacinterp: refactoring using Monad.	Arnaud Spiwack	2014-02-27
\| \| \|	Adds a combinator List.map_right which chains effects from right to left.
*	Remove unsafe code (Obj.magic) in Tacinterp.	Arnaud Spiwack	2014-02-27
	This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).