From 0d8a11017e45ff9b0b18af1d6cd69c66184b55ae Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Sun, 2 Mar 2014 14:17:09 +0100
Subject: 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.
---
 plugins/quote/quote.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 21b221318e..affe31d790 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -107,7 +107,7 @@ open Names
 open Term
 open Pattern
 open Patternops
-open Matching
+open ConstrMatching
 open Tacmach
 open Proofview.Notations
 (*i*)
-- 
cgit v1.2.3