aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/typeclasses.ml')
-rw-r--r--pretyping/typeclasses.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index eabef36417..c8a99a315a 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -118,7 +118,7 @@ let dest_class_app env c =
global_class_of_constr env cl, args
let dest_class_arity env c =
- let rels, c = decompose_prod_assum c in
+ let rels, c = Term.decompose_prod_assum c in
rels, dest_class_app env c
let class_of_constr c = try Some (dest_class_arity (Global.env ()) c) with _ -> None