aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacexpr.ml
Commit message (Expand)AuthorAge
* Strict focusing using Default Goal Selector.Gravatar Gaƫtan Gilbert2018-04-29
* [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
* [ssreflect] Fix module scoping problems due to packing and mli files.Gravatar Emilio Jesus Gallego Arias2018-03-10