aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/vernacexpr.ml
Commit message (Expand)AuthorAge
* Merge PR #7338: [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Pierre-Marie Pédrot2018-05-04
|\
* | [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 `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
|/
* [api] Relocate `intf` modules according to dependency-order.Gravatar Emilio Jesus Gallego Arias2018-04-23