aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/topconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/topconstr.ml')
-rw-r--r--interp/topconstr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index ed44e66ff..0f894019b 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -33,7 +33,7 @@ let _ = Goptions.declare_bool_option {
(* Miscellaneous *)
let error_invalid_pattern_notation ?loc =
- user_err ?loc "" (str "Invalid notation for pattern.")
+ user_err ?loc (str "Invalid notation for pattern.")
(**********************************************************************)
(* Functions on constr_expr *)
@@ -175,7 +175,7 @@ let split_at_annot bl na =
| LocalRawDef _ as x :: rest -> aux (x :: acc) rest
| LocalPattern _ :: rest -> assert false
| [] ->
- user_err ~loc ""
+ user_err ~loc
(str "No parameter named " ++ Nameops.pr_id id ++ str".")
in aux [] bl