aboutsummaryrefslogtreecommitdiff
path: root/pretyping/constrMatching.ml
AgeCommit message (Expand)Author
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-10-10Make constrMatching and detyping more robust with respect toMatthieu Sozeau
2014-09-27Fix semantics of matching with folded/unfolded projections to definitelyMatthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-19Fixes in Ltac pattern-matching on primitive projectionsMatthieu Sozeau
2014-09-18Fix constrMatching as well as change/e_contextually to allowMatthieu Sozeau
2014-09-15Fix bug #3621, using fold_left2 on arrays of the same size only.Matthieu Sozeau
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-04Fix bug #3561, correct folding of env in context[] matching.Matthieu Sozeau
2014-09-04Fix bug #3563, making syntactic matching of primitive projectionsMatthieu Sozeau
2014-09-02Fixing bug #3136.Pierre-Marie Pédrot
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
2014-08-09Allow pattern matching on the applied form of projections with primitiveMatthieu Sozeau
2014-06-15Change Ltac constr matching semantics to consider universes when merging twoMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 15:39:47 +0000