| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-09-05 | Adding a Ftactic module for potentially focussing tactics. | Pierre-Marie Pédrot | |
| 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. | |||
| 2014-02-27 | Tacinterp: more refactoring. | Arnaud Spiwack | |
| Introducing List.fold_right and List.fold_left in Monad. | |||
| 2014-02-27 | Tacinterp: refactoring using Monad. | Arnaud Spiwack | |
| Adds a combinator List.map_right which chains effects from right to left. | |||
| 2014-02-27 | Remove unsafe code (Obj.magic) in Tacinterp. | Arnaud Spiwack | |
| This commit also introduces a module Monad to generate monadic combinators (currently, only List.map). | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |