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 /pretyping | |
| 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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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 |