diff options
| author | herbelin | 2011-04-08 14:08:47 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-08 14:08:47 +0000 |
| commit | 7cc81d4bebb993ea6f71290a808a74439465cdde (patch) | |
| tree | c4aadf8c7116bb7f8c1b6b640771d800923dd10f /toplevel | |
| parent | e1c1d2f9de349abbcd69fe050caad674c561e91a (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 0a93c21c8d..b3f4395cf3 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 = |