aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ssr/ssrcommon.ml
Commit message (Expand)AuthorAge
* Merge PR#513: A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Maxime Dénès2017-06-14
|\
* | Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
| * A fix to #5414 (ident bound by ltac names now known for "match").Gravatar Hugo Herbelin2017-06-09
|/
* Put "ssreflect" behind "API".Gravatar Matej Košík2017-06-07
* Merge the ssr plugin.Gravatar Maxime Dénès2017-06-06