3 files changed, 6 insertions, 6 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index c957ce69fe..0f849e11ab 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -48,7 +48,7 @@ type type_error =
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
-  | IllFormedBranch of constr * int * constr * constr
+  | IllFormedBranch of constr * constructor * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
   | CantApplyBadType of
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index c4e0a92b8b..2bf96f3227 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -48,7 +48,7 @@ type type_error =
   | CaseNotInductive of unsafe_judgment
   | WrongCaseInfo of inductive * case_info
   | NumberBranches of unsafe_judgment * int
-  | IllFormedBranch of constr * int * constr * constr
+  | IllFormedBranch of constr * constructor * constr * constr
   | Generalization of (name * types) * unsafe_judgment
   | ActualType of unsafe_judgment * types
   | CantApplyBadType of
@@ -78,7 +78,7 @@ val error_case_not_inductive : env -> unsafe_judgment -> 'a
 
 val error_number_branches : env -> unsafe_judgment -> int -> 'a
 
-val error_ill_formed_branch : env -> constr -> int -> constr -> constr -> 'a
+val error_ill_formed_branch : env -> constr -> constructor -> constr -> constr -> 'a
 
 val error_generalization : env -> name * types -> unsafe_judgment -> 'a
 
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3568118cf1..85e8e6c885 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -313,11 +313,11 @@ let judge_of_constructor env c =
 
 (* Case. *)
 
-let check_branch_types env cj (lfj,explft) =
+let check_branch_types env ind cj (lfj,explft) =
   try conv_leq_vecti env (Array.map j_type lfj) explft
   with
       NotConvertibleVect i ->
-        error_ill_formed_branch env cj.uj_val i lfj.(i).uj_type explft.(i)
+        error_ill_formed_branch env cj.uj_val (ind,i+1) lfj.(i).uj_type explft.(i)
     | Invalid_argument _ ->
         error_number_branches env cj (Array.length explft)
 
@@ -328,7 +328,7 @@ let judge_of_case env ci pj cj lfj =
   let _ = check_case_info env (fst indspec) ci in
   let (bty,rslty,univ) =
     type_case_branches env indspec pj cj.uj_val in
-  let univ' = check_branch_types env cj (lfj,bty) in
+  let univ' = check_branch_types env (fst indspec) cj (lfj,bty) in
   ({ uj_val  = mkCase (ci, (*nf_betaiota*) pj.uj_val, cj.uj_val,
                        Array.map j_val lfj);
      uj_type = rslty },