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

---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/quote')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 64166a0de6..1299c99ef5 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -107,7 +107,7 @@ open Names
 open Term
 open Pattern
 open Patternops
-open ConstrMatching
+open Constr_matching
 open Tacmach
 (*i*)
 
-- 
cgit v1.2.3