aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/coqloop.ml
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-06 00:24:57 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-06-06 00:24:57 +0200
commitcc0f9d254c394db742473299336fb20b82ae4aa1 (patch)
treecbc89906c862624d4285f367d1fa9f0f61f16f05 /toplevel/coqloop.ml
parentb377bd30f23f430882902f534eaf31b1314ecd07 (diff)
parent88fdd28815747520bdc555a2d1b8600e114ab341 (diff)
Merge PR#716: Don't double up on periods in anomalies
Diffstat (limited to 'toplevel/coqloop.ml')
-rw-r--r--toplevel/coqloop.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 8806c7356..908786565 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -85,7 +85,7 @@ module TopErr = struct
let get_bols_of_loc ibuf (bp,ep) =
let add_line (b,e) lines =
- if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location");
+ if b < 0 || e < b then CErrors.anomaly (Pp.str "Bad location.");
match lines with
| ([],None) -> ([], Some (b,e))
| (fl,oe) -> ((b,e)::fl, oe)