diff options
Diffstat (limited to 'ltac/g_ltac.ml4')
| -rw-r--r-- | ltac/g_ltac.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4 index 9f2c0a93e..c67af33e2 100644 --- a/ltac/g_ltac.ml4 +++ b/ltac/g_ltac.ml4 @@ -36,8 +36,8 @@ let genarg_of_uconstr c = in_gen (rawwit Constrarg.wit_uconstr) c let reference_to_id = function | Libnames.Ident (loc, id) -> (loc, id) | Libnames.Qualid (loc,_) -> - CErrors.user_err_loc (loc, "", - str "This expression should be a simple identifier.") + CErrors.user_err ~loc + (str "This expression should be a simple identifier.") let tactic_mode = Gram.entry_create "vernac:tactic_command" |