diff options
| author | msozeau | 2010-01-14 13:31:31 +0000 |
|---|---|---|
| committer | msozeau | 2010-01-14 13:31:31 +0000 |
| commit | 0fe2a187b9d6b7483e64a662dfeddcfa1c0bc7a4 (patch) | |
| tree | 07cf3a6f549c4bf4d7ebf4a6fbcdbec78aa6ae9e /plugins | |
| parent | 8dc08fad7f99f48837e2e617f4d484364f7f8fc3 (diff) | |
Fix bug #2086, error message when we match on an non-inductive type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12669 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 6c69186648..60e8cb0f7c 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1535,7 +1535,11 @@ let constr_of_pat env isevars arsign pat avoid = PatVar (l, name), [name, None, ty] @ realargs, mkRel 1, ty, (List.map (fun x -> mkRel 1) realargs), 1, avoid | PatCstr (l,((_, i) as cstr),args,alias) -> let cind = inductive_of_constructor cstr in - let IndType (indf, _) = find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) in + let IndType (indf, _) = + try find_rectype env ( !isevars) (lift (-(List.length realargs)) ty) + with Not_found -> error_case_not_inductive env + {uj_val = ty; uj_type = Typing.type_of env !isevars ty} + in let ind, params = dest_ind_family indf in if ind <> cind then error_bad_constructor_loc l cstr ind; let cstrs = get_constructors env indf in |