From 0fe2a187b9d6b7483e64a662dfeddcfa1c0bc7a4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 14 Jan 2010 13:31:31 +0000
Subject: 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
---
 plugins/subtac/subtac_cases.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3