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 8421a05434..5aaa47847d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -166,7 +166,7 @@ in let find_case_dep_nparams env sigma (c,p) (IndFamily (mis,_) as indf) typP = let kelim = mis_kelim mis in let arsign,s = get_arity indf in - let glob_t = prod_it (mkSort s) arsign in + let glob_t = it_mkProd_or_LetIn (mkSort s) arsign in let (dep,_) = is_correct_arity env sigma kelim (c,p) indf (typP,glob_t) in dep |