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 /interp | |
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 'interp')
-rw-r--r-- | interp/constrexpr_ops.ml | 6 | ||||
-rw-r--r-- | interp/constrextern.ml | 2 | ||||
-rw-r--r-- | interp/constrintern.ml | 4 | ||||
-rw-r--r-- | interp/coqlib.ml | 2 | ||||
-rw-r--r-- | interp/implicit_quantifiers.ml | 2 | ||||
-rw-r--r-- | interp/notation.ml | 6 | ||||
-rw-r--r-- | interp/notation_ops.ml | 4 | ||||
-rw-r--r-- | interp/reserve.ml | 2 | ||||
-rw-r--r-- | interp/smartlocate.ml | 2 | ||||
-rw-r--r-- | interp/syntax_def.ml | 2 | ||||
-rw-r--r-- | interp/topconstr.ml | 2 |
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 |