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
---
 toplevel/obligations.ml   | 2 +-
 toplevel/vernacentries.ml | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 750f7a60cb..1be5226deb 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -262,7 +262,7 @@ let pperror cmd = CErrors.errorlabstrm "Program" cmd
 let error s = pperror (str s)
 
 let reduce c =
-  Reductionops.clos_norm_flags Closure.betaiota (Global.env ()) Evd.empty c
+  Reductionops.clos_norm_flags CClosure.betaiota (Global.env ()) Evd.empty c
 
 exception NoObligations of Id.t option
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 04c01f3cd1..e4a2ca5a02 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1287,8 +1287,8 @@ let _ =
       optdepr  = false;
       optname  = "kernel term sharing";
       optkey   = ["Kernel"; "Term"; "Sharing"];
-      optread  = (fun () -> !Closure.share);
-      optwrite = (fun b -> Closure.share := b) }
+      optread  = (fun () -> !CClosure.share);
+      optwrite = (fun b -> CClosure.share := b) }
 
 (* No more undo limit in the new proof engine.
    The command still exists for compatibility (e.g. with ProofGeneral) *)
-- 
cgit v1.2.3