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/funind/invfun.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1ff254f6ca..ad5d077d63 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -8,7 +8,7 @@
 
 open Tacexpr
 open Declarations
-open Errors
+open CErrors
 open Util
 open Names
 open Term
@@ -65,16 +65,16 @@ let observe strm =
 let do_observe_tac s tac g =
   let goal =
     try Printer.pr_goal g
-    with e when Errors.noncritical e -> assert false
+    with e when CErrors.noncritical e -> assert false
   in
   try
     let v = tac g in
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
-    let reraise = Errors.push reraise in
+    let reraise = CErrors.push reraise in
     let e = Cerrors.process_vernac_interp_error reraise in
     observe (hov 0 (str "observation "++ s++str " raised exception " ++
-	     Errors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
+	     CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
 
 
@@ -585,7 +585,7 @@ let rec reflexivity_with_destruct_cases g =
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
         | _ -> Proofview.V82.of_tactic reflexivity
-    with e when Errors.noncritical e -> Proofview.V82.of_tactic reflexivity
+    with e when CErrors.noncritical e -> Proofview.V82.of_tactic reflexivity
   in
   let eq_ind = make_eq () in
   let discr_inject =
@@ -998,7 +998,7 @@ let invfun qhyp f  =
   let f =
     match f with
       | ConstRef f -> f
-      | _ -> raise (Errors.UserError("",str "Not a function"))
+      | _ -> raise (CErrors.UserError("",str "Not a function"))
   in
   try
     let finfos = find_Function_infos f in
-- 
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/funind/invfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ad5d077d63..e0c60d6d5c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -90,7 +90,7 @@ let observe_tac s tac g =
 
 (* [nf_zeta] $\zeta$-normalization of a term *)
 let nf_zeta =
-  Reductionops.clos_norm_flags  (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
+  Reductionops.clos_norm_flags  (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
     Environ.empty_env
     Evd.empty
 
-- 
cgit v1.2.3


From 3ce70f21a18cc19e720e8ac54b93652527881942 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey
Date: Mon, 27 Jun 2016 18:15:07 +0200
Subject: rename toplevel/cerror.ml into explainErr.ml (too close to the new
 lib/cErrors.ml)

---
 plugins/funind/invfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e0c60d6d5c..26fc88a604 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -72,7 +72,7 @@ let do_observe_tac s tac g =
     msgnl (goal ++ fnl () ++ s ++(str " ")++(str "finished")); v
   with reraise ->
     let reraise = CErrors.push reraise in
-    let e = Cerrors.process_vernac_interp_error reraise in
+    let e = ExplainErr.process_vernac_interp_error reraise in
     observe (hov 0 (str "observation "++ s++str " raised exception " ++
 	     CErrors.iprint e ++ str " on goal" ++ fnl() ++ goal ));
     iraise reraise;;
-- 
cgit v1.2.3