aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticMatching.ml
AgeCommit message (Expand)Author
2013-11-19Optimization: in case of empty substitution, merging is trivial.Pierre-Marie Pédrot
2013-11-16Slightly faster version of merging substitutions in TacticMatching.ppedrot
2013-11-14Implementation of Ltac's match and match goal fully based on IStream.aspiwack