aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacexpr.ml
AgeCommit message (Expand)Author
2018-05-01[api] Move bullets and goals selectors to `proofs/`Emilio Jesus Gallego Arias
2018-04-29Strict focusing using Default Goal Selector.Gaƫtan Gilbert
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-03-10[ssreflect] Fix module scoping problems due to packing and mli files.Emilio Jesus Gallego Arias