diff options
| -rw-r--r-- | kernel/type_errors.ml | 2 | ||||
| -rw-r--r-- | kernel/type_errors.mli | 4 | ||||
| -rw-r--r-- | kernel/typeops.ml | 6 | ||||
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 2 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | pretyping/typing.ml | 6 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 9 |
8 files changed, 18 insertions, 24 deletions
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index c957ce69f..0f849e11a 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 c4e0a92b8..2bf96f322 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 3568118cf..85e8e6c88 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 }, diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index 509a4e9e5..a842f36eb 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -79,11 +79,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct i lna vdefj lar done - let check_branches_message loc env evdref c (explft,lft) = + let check_branches_message loc env evdref ind c (explft,lft) = for i = 0 to Array.length explft - 1 do if not (e_cumul env evdref lft.(i) explft.(i)) then let sigma = !evdref in - error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i) + error_ill_formed_branch_loc loc env sigma c (ind,i) lft.(i) explft.(i) done (* coerce to tycon if any *) @@ -96,7 +96,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* let evar_type_case evdref env ct pt lft p c = let (mind,bty,rslty) = type_case_branches env ( evdref) ct pt p c - in check_branches_message evdref env (c,ct) (bty,lft); (mind,rslty) + in check_branches_message evdref env mind (c,ct) (bty,lft); (mind,rslty) *) let strip_meta id = (* For Grammar v7 compatibility *) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 30ee6aaf6..3a3dccb4b 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -74,7 +74,7 @@ val error_case_not_inductive_loc : val error_ill_formed_branch_loc : loc -> env -> Evd.evar_map -> - constr -> int -> constr -> constr -> 'b + constr -> constructor -> constr -> constr -> 'b val error_number_branches_loc : loc -> env -> Evd.evar_map -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index aefa7dfd4..42dd243d0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -221,13 +221,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct i lna vdefj lar done - let check_branches_message loc env evdref c (explft,lft) = - for i = 0 to Array.length explft - 1 do - if not (e_cumul env evdref lft.(i) explft.(i)) then - let sigma = !evdref in - error_ill_formed_branch_loc loc env sigma c i lft.(i) explft.(i) - done - (* coerce to tycon if any *) let inh_conv_coerce_to_tycon loc env evdref j = function | None -> j diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c39be8b68..b40605f22 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -50,12 +50,12 @@ let e_judge_of_apply env evdref funj argjv = in apply_rec 1 funj.uj_type (Array.to_list argjv) -let check_branch_types env evdref cj (lfj,explft) = +let check_branch_types env evdref ind cj (lfj,explft) = if Array.length lfj <> Array.length explft then error_number_branches env cj (Array.length explft); for i = 0 to Array.length explft - 1 do if not (Evarconv.e_cumul env evdref lfj.(i).uj_type explft.(i)) then - 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) done let e_judge_of_case env evdref ci pj cj lfj = @@ -64,7 +64,7 @@ let e_judge_of_case env evdref ci pj cj lfj = with Not_found -> error_case_not_inductive env cj in let _ = check_case_info env (fst indspec) ci in let (bty,rslty,univ) = type_case_branches env indspec pj cj.uj_val in - check_branch_types env evdref cj (lfj,bty); + check_branch_types env evdref (fst indspec) cj (lfj,bty); { uj_val = mkCase (ci, pj.uj_val, cj.uj_val, Array.map j_val lfj); uj_type = rslty } diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 0a93c21c8..b3f4395cf 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -132,16 +132,17 @@ let explain_number_branches env sigma cj expn = str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches." -let explain_ill_formed_branch env sigma c i actty expty = +let explain_ill_formed_branch env sigma c ci actty expty = let simp t = Reduction.nf_betaiota (nf_evar sigma t) in let c = nf_evar sigma c in let env = make_all_name_different env in let pc = pr_lconstr_env env c in let pa = pr_lconstr_env env (simp actty) in let pe = pr_lconstr_env env (simp expty) in - str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the " ++ nth (i+1) ++ str " branch has type" ++ - brk(1,1) ++ pa ++ spc () ++ + strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++ + spc () ++ strbrk "the branch for constructor" ++ spc () ++ + quote (pr_constructor env ci) ++ + spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe ++ str "." let explain_generalization env (name,var) j = |