aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2016-06-27 11:03:43 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-03 12:08:03 +0200
commitf14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch)
tree8a331593d0d1b518e8764c92ac54e3b11c222358 /plugins/syntax
parent500d38d0887febb614ddcadebaef81e0c7942584 (diff)
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
Diffstat (limited to 'plugins/syntax')
-rw-r--r--plugins/syntax/ascii_syntax.ml2
-rw-r--r--plugins/syntax/nat_syntax.ml2
-rw-r--r--plugins/syntax/numbers_syntax.ml4
-rw-r--r--plugins/syntax/z_syntax.ml2
4 files changed, 5 insertions, 5 deletions
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index 03b49e333..e18d19ced 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -11,7 +11,7 @@ let __coq_plugin_name = "ascii_syntax_plugin"
let () = Mltop.add_known_module __coq_plugin_name
open Pp
-open Errors
+open CErrors
open Util
open Names
open Glob_term
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 89305838b..a9eb126b4 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -17,7 +17,7 @@ open Glob_term
open Bigint
open Coqlib
open Pp
-open Errors
+open CErrors
(*i*)
(**********************************************************************)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 57cb2f897..f65f9b791 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.ml
@@ -100,7 +100,7 @@ let int31_of_pos_bigint dloc n =
GApp (dloc, ref_construct, List.rev (args 31 n))
let error_negative dloc =
- Errors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
+ CErrors.user_err_loc (dloc, "interp_int31", Pp.str "int31 are only non-negative numbers.")
let interp_int31 dloc n =
if is_pos_or_zero n then
@@ -189,7 +189,7 @@ let bigN_of_pos_bigint dloc n =
GApp (dloc, ref_constructor, args)
let bigN_error_negative dloc =
- Errors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
+ CErrors.user_err_loc (dloc, "interp_bigN", Pp.str "bigN are only non-negative numbers.")
let interp_bigN dloc n =
if is_pos_or_zero n then
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index ce86c0a65..60803a369 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Bigint