aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
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 /interp
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 'interp')
-rw-r--r--interp/constrexpr_ops.ml6
-rw-r--r--interp/constrextern.ml2
-rw-r--r--interp/constrintern.ml4
-rw-r--r--interp/coqlib.ml2
-rw-r--r--interp/implicit_quantifiers.ml2
-rw-r--r--interp/notation.ml6
-rw-r--r--interp/notation_ops.ml4
-rw-r--r--interp/reserve.ml2
-rw-r--r--interp/smartlocate.ml2
-rw-r--r--interp/syntax_def.ml2
-rw-r--r--interp/topconstr.ml2
11 files changed, 17 insertions, 17 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index f49ed9a5f..04429851f 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -382,18 +382,18 @@ let rec prod_constr_expr c = function
let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
- Errors.user_err_loc (loc, "coerce_reference_to_id",
+ CErrors.user_err_loc (loc, "coerce_reference_to_id",
str "This expression should be a simple identifier.")
let coerce_to_id = function
| CRef (Ident (loc,id),_) -> (loc,id)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_id",
str "This expression should be a simple identifier.")
let coerce_to_name = function
| CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_,_,_) -> (loc,Anonymous)
- | a -> Errors.user_err_loc
+ | a -> CErrors.user_err_loc
(constr_loc a,"coerce_to_name",
str "This expression should be a name.")
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 99b229251..747687189 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 74de6f67f..470eb8324 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -779,7 +779,7 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id =
let scopes = find_arguments_scope ref in
Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var";
GRef (loc, ref, None), impls, scopes, []
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
(* [id] a goal variable *)
GVar (loc,id), [], [], []
diff --git a/interp/coqlib.ml b/interp/coqlib.ml
index 23bcddaea..588637b76 100644
--- a/interp/coqlib.ml
+++ b/interp/coqlib.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index b50732e4e..10cfbe58f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -9,7 +9,7 @@
(*i*)
open Names
open Decl_kinds
-open Errors
+open CErrors
open Util
open Glob_term
open Constrexpr
diff --git a/interp/notation.ml b/interp/notation.ml
index d42307040..0798d385d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Bigint
@@ -208,7 +208,7 @@ let remove_delimiters scope =
let sc = find_scope scope in
let newsc = { sc with delimiters = None } in
match sc.delimiters with
- | None -> Errors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
+ | None -> CErrors.errorlabstrm "" (str "No bound key for scope " ++ str scope ++ str ".")
| Some key ->
scope_map := String.Map.add scope newsc !scope_map;
try
@@ -1056,6 +1056,6 @@ let with_notation_protection f x =
let fs = freeze false in
try let a = f x in unfreeze fs; a
with reraise ->
- let reraise = Errors.push reraise in
+ let reraise = CErrors.push reraise in
let () = unfreeze fs in
iraise reraise
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index d8e022ce6..198bd2216 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -111,7 +111,7 @@ let rec eq_notation_constr t1 t2 = match t1, t2 with
(* Re-interpret a notation as a glob_constr, taking care of binders *)
let name_to_ident = function
- | Anonymous -> Errors.error "This expression should be a simple identifier."
+ | Anonymous -> CErrors.error "This expression should be a simple identifier."
| Name id -> id
let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
diff --git a/interp/reserve.ml b/interp/reserve.ml
index 7e42c1a22..388ca0805 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -8,7 +8,7 @@
(* Reserved names *)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 1f28ba656..478774219 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -13,7 +13,7 @@
(* *)
open Pp
-open Errors
+open CErrors
open Libnames
open Globnames
open Misctypes
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7170fd14a..f96d8acc1 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Errors
+open CErrors
open Util
open Pp
open Names
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 4109bdb7f..2b860173a 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -8,7 +8,7 @@
(*i*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops