aboutsummaryrefslogtreecommitdiff
path: root/tactics/redexpr.ml
AgeCommit message (Collapse)Author
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime Dénès
One other call still remains, but will require to refactor some section-handling code.
2018-12-11[api] Move reduction modules to `tactics`Emilio Jesus Gallego Arias
These modules do actually belong there. We have to slightly reorganize printers, removing a couple of duplicated ones in the way.