From f14b6f1a17652566f0cbc00ce81421ba0684dad5 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Jun 2016 11:03:43 +0200
Subject: errors.ml renamed into cErrors.ml (avoid clash with an OCaml
 compiler-lib module)

 For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
---
 plugins/rtauto/proof_search.ml | 2 +-
 plugins/rtauto/refl_tauto.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index f3eae5f501..8b92611136 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_search.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Goptions
 
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index bb9266db1d..7367a47eaa 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -8,7 +8,7 @@
 
 module Search = Explore.Make(Proof_search)
 
-open Errors
+open CErrors
 open Util
 open Term
 open Tacmach
-- 
cgit v1.2.3


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
---
 plugins/rtauto/refl_tauto.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/rtauto')

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 7367a47eaa..4ed9079517 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -67,12 +67,12 @@ let l_D_Or = lazy (constant "D_Or")
 
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos Closure.all (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos Closure.betaiotazeta (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 type atom_env=
     {mutable next:int;
-- 
cgit v1.2.3