aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-13 23:23:17 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-13 23:23:17 +0000
commit12c4460c3518e643977ac9ca3e872d941abf5833 (patch)
tree5144e962d2336945681e531a264212d24d3678bf /toplevel/command.ml
parentede35d97c697fb52d7edc17556e9089c0eb8f5dc (diff)
fix the 'decreasing on Xth' message
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10661 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 210a79b08..327fe904e 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -656,7 +656,7 @@ let pr_rank = function
| 0 -> str "1st"
| 1 -> str "2nd"
| 2 -> str "3rd"
- | n -> str ((string_of_int n)^"th")
+ | n -> str ((string_of_int (n+1))^"th")
let recursive_message indexes = function
| [] -> anomaly "no recursive definition"