From 5155de9ee4bd01127a57c36cebbd01c5d903d048 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Tue, 26 Sep 2006 08:43:22 +0000
Subject: fixed error mesg in decl mode

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9177 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/decl_proof_instr.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 26a2bd48e9..e7acd6d646 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -1001,7 +1001,9 @@ let rec add_branch env ((id,_) as cpl) pats tree=
 			      br.(pred cnum) in
 			    Split (ids,ind,br)
 		      | Split (ids,ind0,br0) ->
-			  assert (ind=ind0);
+			  if (ind <> ind0) then error
+			    (* this can happen with coercions *)
+	                      "Case pattern belongs to wrong inductive type";
 			  let br=Array.copy br0 in
 			  let ca = constructor_arities env ind in
 			  let _= br.(pred cnum)<-
-- 
cgit v1.2.3