diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2016-06-27 11:03:43 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2016-07-03 12:08:03 +0200 |
commit | f14b6f1a17652566f0cbc00ce81421ba0684dad5 (patch) | |
tree | 8a331593d0d1b518e8764c92ac54e3b11c222358 /plugins/syntax | |
parent | 500d38d0887febb614ddcadebaef81e0c7942584 (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.ml | 2 | ||||
-rw-r--r-- | plugins/syntax/nat_syntax.ml | 2 | ||||
-rw-r--r-- | plugins/syntax/numbers_syntax.ml | 4 | ||||
-rw-r--r-- | plugins/syntax/z_syntax.ml | 2 |
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 |