aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticMatching.mli
AgeCommit message (Expand)Author
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack