aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction/extract_env.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/extraction/extract_env.ml')
-rw-r--r--plugins/extraction/extract_env.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 39826d744..89c2a0ae3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -132,7 +132,7 @@ let rec add_labels mp = function
exception Impossible
let check_arity env cb =
- let t = Typeops.type_of_constant_type env cb.const_type in
+ let t = cb.const_type in
if Reduction.is_arity env t then raise Impossible
let check_fix env cb i =