aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
diff options
context:
space:
mode:
Diffstat (limited to 'checker')
-rw-r--r--checker/check.ml2
-rw-r--r--checker/check.mllib2
-rw-r--r--checker/checker.ml10
-rw-r--r--checker/environ.ml2
-rw-r--r--checker/include2
-rw-r--r--checker/indtypes.ml2
-rw-r--r--checker/inductive.ml2
-rw-r--r--checker/modops.ml2
-rw-r--r--checker/reduction.ml2
-rw-r--r--checker/safe_typing.ml4
-rw-r--r--checker/subtyping.ml6
-rw-r--r--checker/term.ml2
-rw-r--r--checker/typeops.ml2
-rw-r--r--checker/univ.ml2
14 files changed, 21 insertions, 21 deletions
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$.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-21 01:25:57 +0000