From cf95f2a791c263c7aaa3b488d1b09eaafc29be2b Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Jun 2016 16:30:32 +0200
Subject: closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs
 module)

 For the moment, there is a Closure module in compiler-libs/ocamloptcomp.cm(x)a
---
 kernel/reduction.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/reduction.ml')

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 67b05e5262..6c664f7918 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -21,7 +21,7 @@ open Names
 open Term
 open Vars
 open Environ
-open Closure
+open CClosure
 open Esubst
 open Context.Rel.Declaration
 
@@ -318,7 +318,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
 	   convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
        with NotConvertible ->
            (* else the oracle tells which constant is to be expanded *)
-	 let oracle = Closure.oracle_of_infos infos in
+	 let oracle = CClosure.oracle_of_infos infos in
          let (app1,app2) =
            if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
 	     match unfold_reference infos fl1 with
@@ -537,7 +537,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
   else raise NotConvertible
 
 let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
-  let reds = Closure.RedFlags.red_add_transparent betaiotazeta trans in
+  let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
   let infos = create_clos_infos ~evars reds env in
   ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
 
-- 
cgit v1.2.3