diff options
| author | herbelin | 2006-02-07 22:50:35 +0000 |
|---|---|---|
| committer | herbelin | 2006-02-07 22:50:35 +0000 |
| commit | b2dd8c5ffa04478438130138b598d4ca5ec2a760 (patch) | |
| tree | faf8c4cdf34d39280aea0f4e24a31f84c3118144 | |
| parent | 1f9ddd740838dc3be259cafc644b9ee753c46ba3 (diff) | |
Messages nth branche
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8005 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/himsg.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 844accb3af..a67fab04b1 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -136,14 +136,18 @@ let explain_number_branches ctx cj expn = str "of type" ++ brk(1,1) ++ pct ++ spc () ++ str "expects " ++ int expn ++ str " branches" +let ordinal n = + let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in + string_of_int n ^ s + let explain_ill_formed_branch ctx c i actty expty = let ctx = make_all_name_different ctx in let pc = pr_lconstr_env ctx c in let pa = pr_lconstr_env ctx actty in let pe = pr_lconstr_env ctx expty in str "In pattern-matching on term" ++ brk(1,1) ++ pc ++ - spc () ++ str "the branch " ++ int (i+1) ++ - str " has type" ++ brk(1,1) ++ pa ++ spc () ++ + spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++ + brk(1,1) ++ pa ++ spc () ++ str "which should be" ++ brk(1,1) ++ pe let explain_generalization ctx (name,var) j = |