aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.mli
Commit message (Collapse)AuthorAge
...
* Moving three related small half-general half-ad-hoc utility functionsGravatar Hugo Herbelin2015-12-05
| | | | | next to each other, waiting for possible integration into a more uniform API.
* Fix documentation.Gravatar Matthieu Sozeau2015-07-27
|
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2015-07-02
|
* Adding a new folder corresponding to the low-level part of the pretyperGravatar Pierre-Marie Pédrot2015-02-27
together with the tactic monad. The move is not complete yet, because some file candidates for this directory have almost useless dependencies in other ones that should not be moved.