aboutsummaryrefslogtreecommitdiff
path: root/kernel/closure.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/closure.ml')
-rw-r--r--kernel/closure.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index e7b1a634fa..f452a6dfc2 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -309,7 +309,7 @@ let fixp_reducible redfun flgs op stk =
false
let mindsp_nparams env sp =
- let mib = lookup_mind sp env in mib.Constant.mind_nparams
+ let mib = lookup_mind sp env in mib.Declarations.mind_nparams
(* The main recursive functions
*