diff options
| author | Pierre-Marie Pédrot | 2016-09-08 14:56:33 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-09-08 15:41:16 +0200 |
| commit | 13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (patch) | |
| tree | f76fd37023c71c20520e34e4a51c487e7a0388a0 /interp/constrexpr_ops.ml | |
| parent | 79e7a0de25bcb2f10a7f3d1960a8f16eefdbb5a6 (diff) | |
| parent | fc579fdc83b751a44a18d2373e86ab38806e7306 (diff) | |
Merge PR #244.
Diffstat (limited to 'interp/constrexpr_ops.ml')
| -rw-r--r-- | interp/constrexpr_ops.ml | 16 |
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.") |
