aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre Letouzey2014-03-02 14:17:09 +0100
committerPierre Letouzey2014-03-02 20:00:03 +0100
commit0d8a11017e45ff9b0b18af1d6cd69c66184b55ae (patch)
tree7c2a4361b949c5f496bdee7d56ce9f8aaa878277 /dev
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 'dev')
-rw-r--r--dev/printers.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 82ef43a7d5..30ac772d0a 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -118,7 +118,7 @@ Evarconv
Arguments_renaming
Typing
Patternops
-Matching
+ConstrMatching
Tacred
Classops
Typeclasses_errors