| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
|
|
| |
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 monadic bind can be costly, so sparing a few can be worth it. Therefore I unrolled the last element of the recursions. I took the opportunity to do some loop unrolling, which is probably more useful for map combinators than for fold.
|
| | |
|
| |
|
|
|
|
| |
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).
|
Arnaud Spiwack
Pierre-Marie Pédrot