diff options
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 475005648..3257d406a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -294,8 +294,8 @@ let find_applied_relation metas loc env sigma c left2right = match decompose_applied_relation metas env sigma c ctype left2right with | Some c -> c | None -> - user_err_loc (loc, "decompose_applied_relation", - str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ + user_err ~loc "decompose_applied_relation" + (str"The type" ++ spc () ++ Printer.pr_constr_env env sigma ctype ++ spc () ++ str"of this term does not end with an applied relation.") (* To add rewriting rules to a base *) |