aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2016-08-19 02:35:47 +0200
committerEmilio Jesus Gallego Arias2016-08-19 02:46:38 +0200
commitfc579fdc83b751a44a18d2373e86ab38806e7306 (patch)
treeb325c2ff65c505ad62ac7b3fce6bce28633a60f0 /interp/constrexpr_ops.ml
parent543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (diff)
Make the user_err header an optional parameter.
Suggested by @ppedrot
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 9097a56f85..59c24900d2 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -382,18 +382,18 @@ let rec prod_constr_expr c = function
let coerce_reference_to_id = function
| Ident (_,id) -> id
| Qualid (loc,_) ->
- CErrors.user_err ~loc "coerce_reference_to_id"
+ CErrors.user_err ~loc ~hdr:"coerce_reference_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_id = function
| CRef (Ident (loc,id),_) -> (loc,id)
| a -> CErrors.user_err ~loc:(constr_loc a)
- "coerce_to_id"
+ ~hdr:"coerce_to_id"
(str "This expression should be a simple identifier.")
let coerce_to_name = function
| CRef (Ident (loc,id),_) -> (loc,Name id)
| CHole (loc,_,_,_) -> (loc,Anonymous)
| a -> CErrors.user_err
- ~loc:(constr_loc a) "coerce_to_name"
+ ~loc:(constr_loc a) ~hdr:"coerce_to_name"
(str "This expression should be a name.")