From f14b6f1a17652566f0cbc00ce81421ba0684dad5 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
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/romega/const_omega.ml |  6 +++---
 plugins/romega/g_romega.ml4   |  2 +-
 plugins/romega/refl_omega.ml  | 12 ++++++------
 3 files changed, 10 insertions(+), 10 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 21b0f78b5..4935fe4bb 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -39,7 +39,7 @@ let destructurate t =
     | Term.Var id,[] -> Kvar(Names.Id.to_string id)
     | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
     | Term.Prod (Names.Name _,_,_),[] ->
-	Errors.error "Omega: Not a quantifier-free goal"
+	CErrors.error "Omega: Not a quantifier-free goal"
     | _ -> Kufo
 
 exception Destruct
@@ -346,7 +346,7 @@ let parse_term t =
     | Kapp("Z.succ",[t]) -> Tsucc t
     | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one))
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) ->
-	(try Tnum (recognize t) with e when Errors.noncritical e -> Tother)
+	(try Tnum (recognize t) with e when CErrors.noncritical e -> Tother)
     | _ -> Tother
   with e when Logic.catchable_exception e -> Tother
 
@@ -368,6 +368,6 @@ let is_scalar t =
     | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t
     | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true
     | _ -> false in
-  try aux t with e when Errors.noncritical e -> false
+  try aux t with e when CErrors.noncritical e -> false
 
 end
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index fd4ede6c3..830dc54dd 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -27,7 +27,7 @@ let romega_tactic l =
        | "positive" -> eval_tactic "zify_positive"
        | "N" -> eval_tactic "zify_N"
        | "Z" -> eval_tactic "zify_op"
-       | s -> Errors.error ("No ROmega knowledge base for type "^s))
+       | s -> CErrors.error ("No ROmega knowledge base for type "^s))
     (Util.List.sort_uniquize String.compare l)
   in
   Tacticals.New.tclTHEN
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index a059512d8..ba882e39a 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -454,7 +454,7 @@ let rec scalar n = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_mult_assoc_reduced], Omult(t1,Oint (n*x))
  | Omult(t1,t2) ->
-     Errors.error "Omega: Can't solve a goal with non-linear products"
+     CErrors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) -> do_list [], Omult(t,Oint n)
  | Oint i -> do_list [Lazy.force coq_c_reduce],Oint(n*i)
  | (Oufo _ as t)-> do_list [], Oufo (Omult(t,Oint n))
@@ -473,7 +473,7 @@ let rec negate = function
  | Omult(t1,Oint x) ->
      do_list [Lazy.force coq_c_opp_mult_r], Omult(t1,Oint (Bigint.neg x))
  | Omult(t1,t2) ->
-     Errors.error "Omega: Can't solve a goal with non-linear products"
+     CErrors.error "Omega: Can't solve a goal with non-linear products"
  | (Oatom _ as t) ->
      do_list [Lazy.force coq_c_opp_one], Omult(t,Oint(negone))
  | Oint i -> do_list [Lazy.force coq_c_reduce] ,Oint(Bigint.neg i)
@@ -545,7 +545,7 @@ let shrink_pair f1 f2 =
        Lazy.force coq_c_red4, Omult(Oatom v,Oplus(c1,c2))
    | t1,t2 ->
        oprint stdout t1; print_newline (); oprint stdout t2; print_newline ();
-       flush Pervasives.stdout; Errors.error "shrink.1"
+       flush Pervasives.stdout; CErrors.error "shrink.1"
   end
 
 (* \subsection{Calcul d'une sous formule constante} *)
@@ -559,9 +559,9 @@ let reduce_factor = function
       let rec compute = function
           Oint n -> n
 	| Oplus(t1,t2) -> compute t1 + compute t2
-	| _ -> Errors.error "condense.1" in
+	| _ -> CErrors.error "condense.1" in
 	[Lazy.force coq_c_reduce], Omult(Oatom v,Oint(compute c))
-  | t -> Errors.error "reduce_factor.1"
+  | t -> CErrors.error "reduce_factor.1"
 
 (* \subsection{Réordonnancement} *)
 
@@ -1304,7 +1304,7 @@ let total_reflexive_omega_tactic gl =
   let systems_list = destructurate_hyps full_reified_goal in
   if !debug then display_systems systems_list;
   resolution env full_reified_goal systems_list gl
-  with NO_CONTRADICTION -> Errors.error "ROmega can't solve this system"
+  with NO_CONTRADICTION -> CErrors.error "ROmega can't solve this system"
 
 
 (*i let tester = Tacmach.hide_atomic_tactic "TestOmega" test_tactic i*)
-- 
cgit v1.2.3