| Commit message (Collapse) | Author | Age |
|
|
|
|
| |
Introduce by myself, I'm afraid, in #308. Noticed by PMP during the
review, but I forgot to fix it before merge.
|
|
|
|
|
|
|
|
| |
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).
|
|
|
| |
Otherwise I risked catching errors from the argument functions when I wanted to catch size mismatch to add information to errors.
|
| |
|
|
|
|
| |
For optimisation purposes.
|
| |
|
|
|
|
|
|
| |
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.
|
|
|
| |
Introducing List.fold_right and List.fold_left in Monad.
|
|
|
| |
Adds a combinator List.map_right which chains effects from right to left.
|
|
This commit also introduces a module Monad to generate monadic combinators (currently, only List.map).
|