From 6eff115a9094104eac9be09eb0e755f98366cf8d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 2 Jan 2005 08:46:18 +0000
Subject: Partie reduction_of_red_expr de tacred.ml qui dépend de la vm
 maintenant dans redexpr.ml

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

(limited to 'contrib/xml/doubleTypeInference.ml')

diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index cf975b4372..728c7ac9a7 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -42,7 +42,7 @@ prerr_endline "###whd_betadeltaiotacprop:" ;
 let xxx =
 (*Pp.msgerr (Printer.prterm_env env ty);*)
 prerr_endline "";
-   Tacred.reduction_of_redexp red_exp env evar_map ty
+   Redexpr.reduction_of_red_expr red_exp env evar_map ty
 in
 prerr_endline "###FINE" ;
 (*
-- 
cgit v1.2.3