aboutsummaryrefslogtreecommitdiff
path: root/tactics/tacticMatching.ml
AgeCommit message (Expand)Author
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-11-22Specific printer of Evar.Set.t for ocamldebug + more information inHugo Herbelin
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-07-28CPS-style tactic matching. We use the tactic monad as the target of the CPS.Pierre-Marie Pédrot
2014-07-22Small code sharing in TacticMatching.Pierre-Marie Pédrot
2014-07-05Using IStream coiterator to explicit the captured state of tactic matching re...Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
2014-02-24TacticMatching: avoid some closure allocation in (<*>).Arnaud Spiwack
2014-02-24Removed some trailing whitespaces.Arnaud Spiwack
2014-02-24IStream: a concat_map primitive.Arnaud Spiwack
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:15:12 +0000