aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/metasyntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/metasyntax.ml')
-rw-r--r--vernac/metasyntax.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index a586fe9f2..feacfe915 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -192,7 +192,7 @@ let parse_format ((loc, str) : lstring) =
error "Empty format."
with reraise ->
let (e, info) = CErrors.push reraise in
- let info = Loc.add_loc info loc in
+ let info = Option.cata (Loc.add_loc info) info loc in
iraise (e, info)
(***********************)