diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index f09ba50ec7..3452be55c3 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -215,7 +215,7 @@ let typecheck_inductive env mie = let lev = (* Decide that if the conclusion is not explicitly Type *) (* then the inductive type is not polymorphic *) - match kind_of_term (snd (decompose_prod_assum arity.utj_val)) with + match kind_of_term ((strip_prod_assum arity.utj_val)) with | Sort (Type u) -> Some u | _ -> None in (cst,env_ar',(id,full_arity,lev)::l)) |