diff options
| author | herbelin | 2006-04-28 07:33:33 +0000 |
|---|---|---|
| committer | herbelin | 2006-04-28 07:33:33 +0000 |
| commit | 0625a1e62f070eb4d13235407eec0b818246b8b9 (patch) | |
| tree | 968f861be1520d2cd353747b00eacdae907c4ac1 | |
| parent | 2915ddeed74a1fb4f44137443742e235d2455931 (diff) | |
Typo dans précédent commit (8755); protection renforcée dans analyse clause in du cases
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8757 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |