diff options
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 40f41d6038..7e81618654 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -349,7 +349,6 @@ let type_of_sort c g = match c with | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g' | DOP0 (Sort (Prop _)) -> mkType prop_univ, g - | DOP0 (Implicit) -> mkImplicit, g | _ -> invalid_arg "type_of_sort" (* Type of a lambda-abstraction. *) @@ -743,6 +742,9 @@ let check_fix env = function (* Co-fixpoints. *) +let mind_nparams env i = + let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams + let check_guard_rec_meta env nbfix def deftype = let rec codomain_is_coind c = match whd_betadeltaiota env (strip_outer_cast c) with |