aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticMatching.ml
Commit message (Expand)AuthorAge
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* TacticMatching: avoid some closure allocation in (<*>).Gravatar Arnaud Spiwack2014-02-24
* Removed some trailing whitespaces.Gravatar Arnaud Spiwack2014-02-24
* IStream: a concat_map primitive.Gravatar Arnaud Spiwack2014-02-24
* Optimization: in case of empty substitution, merging is trivial.Gravatar Pierre-Marie Pédrot2013-11-19
* Slightly faster version of merging substitutions in TacticMatching.Gravatar ppedrot2013-11-16
* Implementation of Ltac's match and match goal fully based on IStream.Gravatar aspiwack2013-11-14