aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/syntax/nat_syntax.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/syntax/nat_syntax.ml')
-rw-r--r--plugins/syntax/nat_syntax.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index a9eb126b4..6d62496ee 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -47,8 +47,8 @@ let nat_of_int dloc n =
mk_nat ref_O n
end
else
- user_err_loc (dloc, "nat_of_int",
- str "Cannot interpret a negative number as a number of type nat")
+ user_err "nat_of_int"
+ (str "Cannot interpret a negative number as a number of type nat")
(************************************************************************)
(* Printing via scopes *)