From d08532d5344d96d10604760fa44109c9d56e73ce Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Thu, 8 Jan 2015 18:18:02 +0100
Subject: Avoiding introducing yet another convention in naming files.

---
 dev/printers.mllib | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'dev')

diff --git a/dev/printers.mllib b/dev/printers.mllib
index 2e61cb697..2f78c2e91 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -132,7 +132,7 @@ Recordops
 Evarconv
 Typing
 Patternops
-ConstrMatching
+Constr_matching
 Find_subterm
 Tacred
 Classops
-- 
cgit v1.2.3