aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2016-09-08 14:56:33 +0200
committerPierre-Marie Pédrot2016-09-08 15:41:16 +0200
commit13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch)
treef76fd37023c71c20520e34e4a51c487e7a0388a0 /interp/constrexpr_ops.ml
parent79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff)
parentfc579fdc83b751a44a18d2373e86ab38806e7306 (diff)
Merge PR #244.
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml16
1 files changed, 8 insertions, 8 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 04429851fd..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 (loc, "coerce_reference_to_id",
- str "This expression should be a simple identifier.")
+ 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",
- str "This expression should be a simple identifier.")
+ | a -> CErrors.user_err ~loc:(constr_loc a)
+ ~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",
- str "This expression should be a name.")
+ | a -> CErrors.user_err
+ ~loc:(constr_loc a) ~hdr:"coerce_to_name"
+ (str "This expression should be a name.")