summaryrefslogtreecommitdiff
path: root/library/kindops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/kindops.ml')
-rw-r--r--library/kindops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/library/kindops.ml b/library/kindops.ml
index c634193d..21b1bec3 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -25,7 +25,7 @@ let string_of_theorem_kind = function
let string_of_definition_kind def =
let (locality, poly, kind) = def in
- let error () = Errors.anomaly (Pp.str "Internal definition kind") in
+ let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
match kind with
| Definition ->
begin match locality with
@@ -64,4 +64,4 @@ let string_of_definition_kind def =
| Global -> "Global Instance"
end
| (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
- Errors.anomaly (Pp.str "Internal definition kind")
+ CErrors.anomaly (Pp.str "Internal definition kind")