aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticMatching.mli
Commit message (Expand)AuthorAge
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Implementation of Ltac's match and match goal fully based on IStream.Gravatar aspiwack2013-11-14