diff options
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ef95fbb5c..610bde687 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -92,7 +92,7 @@ let mis_nf_constructor_type (ind,mib,mip) j = and nconstr = Array.length mip.mind_consnames in let make_Ik k = mkInd ((fst ind),ntypes-k-1) in if j > nconstr then error "Not enough constructors in the type."; - substl (List.tabulate make_Ik ntypes) specif.(j-1) + substl (List.init ntypes make_Ik) specif.(j-1) (* Arity of constructors excluding parameters and local defs *) |