Modification de type_of_case, type_case_branches, etc

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@352 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 1 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 668d16b30..8579b495b 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -121,7 +121,10 @@ and mk_casegoals sigma goal goalacc p c =
   let env = goal.evar_env in
   let (acc',ct) = mk_hdgoals sigma goal goalacc c in 
   let (acc'',pt) = mk_hdgoals sigma goal acc' p in
-  let (_,lbrty,conclty) = type_case_branches env sigma ct pt p c in
+  let indspec =
+    try try_mutind_of env sigma ct
+    with Induc -> anomaly "mk_casegoals" in
+  let (lbrty,conclty) = type_case_branches env sigma indspec pt p c in
   (acc'',lbrty,conclty)