From 8a71afd27620a5d6c507b115d6fd408d879544c5 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:53 +0000
Subject: Pattern as a mli-only file, operations in Patternops

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15376 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/redexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 12aec91425..d0782e970b 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -223,7 +223,7 @@ let subst_red_expr subs e =
   subst_gen_red_expr
     (Mod_subst.subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Pattern.subst_pattern subs)
+    (Patternops.subst_pattern subs)
     e
 
 let inReduction : bool * string * red_expr -> obj =
-- 
cgit v1.2.3