diff options
| author | Emilio Jesus Gallego Arias | 2016-08-19 02:35:47 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2016-08-19 02:46:38 +0200 |
| commit | fc579fdc83b751a44a18d2373e86ab38806e7306 (patch) | |
| tree | b325c2ff65c505ad62ac7b3fce6bce28633a60f0 /interp/constrexpr_ops.ml | |
| parent | 543ee0c7ad43874c577416af9f2e5a94d7d1e4d3 (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.ml | 6 |
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.") |
