From 7cc81d4bebb993ea6f71290a808a74439465cdde Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 8 Apr 2011 14:08:47 +0000
Subject: Replaced printing number of ill-typed branch by printing name of
 constructor when a "match" is kernel-ill-typed (probably rarely visible from
 end user anyway but useful for debugging) + dead code.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typeops.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/typeops.ml')

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