diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index c6355b3ea..49f883628 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -115,7 +115,7 @@ let check_hyps_inclusion env c sign = let extract_level env p = let _,c = dest_prod_assum env p in - match kind_of_term c with Sort (Type u) -> Some u | _ -> None + match kind_of_term c with Sort (Type u) -> Univ.Universe.level u | _ -> None let extract_context_levels env l = let fold l (_, b, p) = match b with |