aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacexpr.ml
Commit message (Expand)AuthorAge
* Tactic deprecation machineryGravatar Maxime Dénès2018-07-12
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* [api] Remove Misctypes.Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: move Tactypes to proofsGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Misctypes removal: multi to tactics/rewriteGravatar Emilio Jesus Gallego Arias2018-06-12
* [api] Move bullets and goals selectors to `proofs/`Gravatar Emilio Jesus Gallego Arias2018-05-01
* 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