aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/g_prim.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/g_prim.ml4')
-rw-r--r--parsing/g_prim.ml44
1 files changed, 2 insertions, 2 deletions
diff --git a/parsing/g_prim.ml4 b/parsing/g_prim.ml4
index b90e06cd3..820514b08 100644
--- a/parsing/g_prim.ml4
+++ b/parsing/g_prim.ml4
@@ -28,7 +28,7 @@ let my_int_of_string loc s =
if n > 1024 * 2048 then raise Exit;
n
with Failure _ | Exit ->
- CErrors.user_err_loc (loc,"",Pp.str "Cannot support a so large number.")
+ CErrors.user_err ~loc (Pp.str "Cannot support a so large number.")
GEXTEND Gram
GLOBAL:
@@ -93,7 +93,7 @@ GEXTEND Gram
;
ne_string:
[ [ s = STRING ->
- if s="" then CErrors.user_err_loc(!@loc, "", Pp.str"Empty string."); s
+ if s="" then CErrors.user_err ~loc:(!@loc) (Pp.str"Empty string."); s
] ]
;
ne_lstring: