diff options
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index db5458211d..96fe8d5846 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -110,7 +110,7 @@ let listrec_mconstr env ntypes nparams i indlc = let (lpar,auxlargs) = array_chop auxnpar largs in if not (array_for_all (noccur_bet n ntypes) auxlargs) then raise (InductiveError (NonPos n)); - let auxlc = mis_lc env mispeci + let auxlc = mis_lc mispeci and auxntyp = mis_ntypes mispeci in if auxntyp <> 1 then raise (InductiveError (NonPos n)); let lrecargs = array_map_to_list (check_param_pos n) lpar in |