From 2a20061cc2790eedee7fab6230fe1dd2b4d58c24 Mon Sep 17 00:00:00 2001
From: xclerc
Date: Mon, 14 Oct 2013 08:32:27 +0000
Subject: Remove some uses of local modules (some were unused, some were
 costly).

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

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

diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index 5a3880b015..d543081658 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.ml
@@ -16,20 +16,17 @@
 type types = {synthesized : Term.types ; expected : Term.types option};;
 
 let cprop =
- let module N = Names in
-  N.make_con
-   (N.MPfile
+  Names.make_con
+   (Names.MPfile
      (Libnames.dirpath_of_string "CoRN.algebra.CLogic"))
-   (N.DirPath.empty)
-   (N.Label.make "CProp")
+   (Names.DirPath.empty)
+   (Names.Label.make "CProp")
 ;;
 
 let whd_betadeltaiotacprop env _evar_map ty =
- let module C = Closure in
- let module CR = C.RedFlags in
  (*** CProp is made Opaque ***)
- let flags = CR.red_sub C.betadeltaiota (CR.fCONST cprop) in
- C.whd_val (C.create_clos_infos flags env) (C.inject ty)
+ let flags = Closure.RedFlags.red_sub Closure.betadeltaiota (Closure.RedFlags.fCONST cprop) in
+ Closure.whd_val (Closure.create_clos_infos flags env) (Closure.inject ty)
 ;;
 
 
-- 
cgit v1.2.3