aboutsummaryrefslogtreecommitdiff
path: root/tactics/ppred.ml
AgeCommit message (Collapse)Author
2019-02-08locus: Add an AtLeastOneOccurrence constructor.Matthieu Sozeau
The semantics is obviously that it is an error if not at least one occurrence is found (natural semantics for rewriting for example).
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.