aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/heads.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/heads.ml')
-rw-r--r--library/heads.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/library/heads.ml b/library/heads.ml
index 4c9b78976..02465f22f 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -70,7 +70,7 @@ let kind_of_head env t =
| Const (cst,_) ->
(try on_subterm k l b (constant_head cst)
with Not_found ->
- Errors.anomaly
+ CErrors.anomaly
Pp.(str "constant not found in kind_of_head: " ++
str (Names.Constant.to_string cst)))
| Construct _ | CoFix _ ->