aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac/tacexpr.ml
AgeCommit message (Expand)Author
2018-07-12Tactic deprecation machineryMaxime Dénès
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: move Tactypes to proofsEmilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: several moves:Emilio Jesus Gallego Arias
2018-06-12[api] Misctypes removal: multi to tactics/rewriteEmilio Jesus Gallego Arias
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