aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evd.mli
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-03-02 14:17:09 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2014-03-02 20:00:03 +0100
commit0d8a11017e45ff9b0b18af1d6cd69c66184b55ae (patch)
tree7c2a4361b949c5f496bdee7d56ce9f8aaa878277 /pretyping/evd.mli
parent9130ea9cbc657cd7adf02830e40a89f6de3953f3 (diff)
Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)
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.
Diffstat (limited to 'pretyping/evd.mli')
0 files changed, 0 insertions, 0 deletions