diff options
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | pretyping/cases.ml | 5 |
2 files changed, 5 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1e8c7fdef0..98919082df 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -963,7 +963,7 @@ let internalise sigma globalenv env allow_soapp lvar c = if List.exists ((<>) Anonymous) parnal then user_err_loc (loc,"", str "The parameters of inductive type must be implicit"); - (loc,ind,nparams,nal) + (loc,ind,nparams,realnal) | _ -> error_bad_inductive_type (loc_of_rawconstr t) in nal, Some indsign | None -> diff --git a/pretyping/cases.ml b/pretyping/cases.ml index f709ab450e..39b26a2b70 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1546,8 +1546,11 @@ let extract_arity_signature env0 tomatchl tmsign = let realnal = match t with | Some (loc,ind',nparams,realnal) -> - if ind <> ind' or List.length params <> nparams then + if ind <> ind' then user_err_loc (loc,"",str "Wrong inductive type"); + if List.length params <> nparams + or nrealargs <> List.length realnal then + anomaly "Ill-formed 'in' clause in cases"; List.rev realnal | None -> list_tabulate (fun _ -> Anonymous) nrealargs in let arsign = fst (get_arity env0 indf') in |