summaryrefslogtreecommitdiff
path: root/library/kindops.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
committerGravatar Enrico Tassi <gareuselesinge@debian.org>2016-12-27 16:53:30 +0100
commita4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch)
tree26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /library/kindops.ml
parent164c6861860e6b52818c031f901ffeff91fca16a (diff)
Imported Upstream version 8.6upstream/8.6
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")