diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-08-19 02:46:38 +0200 |
| commit | fc579fdc83b751a44a18d2373e86ab38806e7306 (patch) | |
| tree | b325c2ff65c505ad62ac7b3fce6bce28633a60f0 /tactics/autorewrite.ml | |
| parent | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff) | |
Make the user_err header an optional parameter.
Suggested by @ppedrot
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 b898ceb04..7628b7885 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -65,7 +65,7 @@ let raw_find_base bas = String.Map.find bas !rewtab let find_base bas = try raw_find_base bas with Not_found -> - user_err "AutoRewrite" + user_err ~hdr:"AutoRewrite" (str "Rewriting base " ++ str bas ++ str " does not exist.") let find_rewrites bas = @@ -294,7 +294,7 @@ 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 "decompose_applied_relation" + user_err ~loc ~hdr:"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.") |