From a936f2e879ac1f9b2e7e9d8a5376469e3d53c606 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 29 May 2012 11:08:44 +0000
Subject: Glob_term now mli-only, operations now in Glob_ops Stuff about
 reductions now in genredexpr.mli, operations in redops.ml

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

(limited to 'plugins/xml')

diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 30cd5c18b..24a383250 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -27,7 +27,6 @@ let cprop =
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
- let module R = Glob_term in
  let module C = Closure in
  let module CR = C.RedFlags in
  (*** CProp is made Opaque ***)
-- 
cgit v1.2.3