diff options
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 72058f62c7..94a8cc277e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -84,7 +84,7 @@ let mis_type_mconstruct i mispec = and nconstr = mis_nconstr mispec in let make_Ik k = mkMutInd ((mispec.mis_sp,ntypes-k-1),mispec.mis_args) in if i > nconstr then error "Not enough constructors in the type"; - typed_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1) + type_app (substl (list_tabulate make_Ik ntypes)) specif.(i-1) let mis_user_arity mis = let hyps = mis.mis_mib.mind_hyps |