aboutsummaryrefslogtreecommitdiff
path: root/pretyping/constrMatching.mli
AgeCommit message (Collapse)Author
2015-01-08Avoiding introducing yet another convention in naming files.Hugo Herbelin
2014-08-25Fixing bug #3377 by giving env and sigma to constrMathching. Now it's possibleMatthieu Sozeau
to match on a primitive projection application c.(p) using "?f _", binding f to (fun x => x.(p)) with the correct typing.
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
With ocaml 4.01, the 'unused open' warning also checks the mli :-) Beware: some open are reported as useless when compiling with camlp5, but are necessary for compatibility with camlp4. These open are now marked with a comment.
2014-03-02Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Pierre Letouzey
There are currently two other clashs : Lexer and Errors, but for the moment these ones haven't impacted my experiments with extraction and compiler-libs, while this Matching issue had. And anyway the new name is more descriptive, in the spirit of the recent TacticMatching.