From f14b6f1a17652566f0cbc00ce81421ba0684dad5 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey 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 --- checker/check.ml | 2 +- checker/check.mllib | 2 +- checker/checker.ml | 10 +++++----- checker/environ.ml | 2 +- checker/include | 2 +- checker/indtypes.ml | 2 +- checker/inductive.ml | 2 +- checker/modops.ml | 2 +- checker/reduction.ml | 2 +- checker/safe_typing.ml | 4 ++-- checker/subtyping.ml | 6 +++--- checker/term.ml | 2 +- checker/typeops.ml | 2 +- checker/univ.ml | 2 +- 14 files changed, 21 insertions(+), 21 deletions(-) (limited to 'checker') diff --git a/checker/check.ml b/checker/check.ml index da3cd0316..863cf7b2c 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Names diff --git a/checker/check.mllib b/checker/check.mllib index 1925477e0..488507a13 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -34,7 +34,7 @@ Feedback Segmenttree Unicodetable Unicode -Errors +CErrors CWarnings CEphemeron Future diff --git a/checker/checker.ml b/checker/checker.ml index 2c872f272..0c411ae44 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open System open Flags @@ -71,7 +71,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath = let convert_string d = try Id.of_string d - with Errors.UserError _ -> + with CErrors.UserError _ -> if_verbose Feedback.msg_warning (str "Directory " ++ str d ++ str " cannot be used as a Coq identifier (skipped)"); raise Exit @@ -303,7 +303,7 @@ let rec explain_exn = function str ", characters " ++ int e ++ str "-" ++ int (e+6) ++ str ")")) ++ report ()) - | e -> Errors.print e (* for anomalies and other uncaught exceptions *) + | e -> CErrors.print e (* for anomalies and other uncaught exceptions *) let parse_args argv = let rec parse = function @@ -329,7 +329,7 @@ let parse_args argv = | "-debug" :: rem -> set_debug (); parse rem | "-where" :: _ -> - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; print_endline (Envars.coqlib ()); exit 0 @@ -367,7 +367,7 @@ let init_with_argv argv = try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; - Envars.set_coqlib ~fail:Errors.error; + Envars.set_coqlib ~fail:CErrors.error; if_verbose print_header (); init_load_path (); engage (); diff --git a/checker/environ.ml b/checker/environ.ml index 881284eda..7b59c6b98 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -1,4 +1,4 @@ -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/include b/checker/include index f5bd2984e..6bea3c91a 100644 --- a/checker/include +++ b/checker/include @@ -31,7 +31,7 @@ open Typeops;; open Check;; open Pp;; -open Errors;; +open CErrors;; open Util;; open Names;; open Term;; diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 40f55a571..27f79e796 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/inductive.ml b/checker/inductive.ml index 8bbd0f142..cb344c7fd 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/modops.ml b/checker/modops.ml index 442f999bb..b720fb621 100644 --- a/checker/modops.ml +++ b/checker/modops.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Pp open Names diff --git a/checker/reduction.ml b/checker/reduction.ml index 97cf6ca75..ec16aa261 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Cic open Term diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml index e644febe4..11cd742ba 100644 --- a/checker/safe_typing.ml +++ b/checker/safe_typing.ml @@ -7,7 +7,7 @@ (************************************************************************) open Pp -open Errors +open CErrors open Util open Cic open Names @@ -40,7 +40,7 @@ let check_engagement env expected_impredicative_set = begin match impredicative_set, expected_impredicative_set with | PredicativeSet, ImpredicativeSet -> - Errors.error "Needs option -impredicative-set." + CErrors.error "Needs option -impredicative-set." | _ -> () end; () diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 46d21f6cc..7eae9b831 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -7,7 +7,7 @@ (************************************************************************) (*i*) -open Errors +open CErrors open Util open Names open Cic @@ -302,7 +302,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let c2 = force_constr lc2 in check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ @@ -313,7 +313,7 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_conv conv_leq env arity1 typ2 | IndConstr (((kn,i),j) as cstr,mind1) -> - ignore (Errors.error ( + ignore (CErrors.error ( "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ "constructor and give a definition to map the old name to the new " ^ diff --git a/checker/term.ml b/checker/term.ml index 56cc9cdc2..591348cb6 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -8,7 +8,7 @@ (* This module instantiates the structure of generic deBruijn terms to Coq *) -open Errors +open CErrors open Util open Names open Esubst diff --git a/checker/typeops.ml b/checker/typeops.ml index 886689329..173e19ce1 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Errors +open CErrors open Util open Names open Cic diff --git a/checker/univ.ml b/checker/univ.ml index 96d827013..668f3a058 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -14,7 +14,7 @@ (* Revisions by Bruno Barras, Hugo Herbelin, Pierre Letouzey *) open Pp -open Errors +open CErrors open Util (* Universes are stratified by a partial ordering $\le$. -- cgit v1.2.3