aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/decl_mode/decl_interp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
-rw-r--r--plugins/decl_mode/decl_interp.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml
index 9ed5c61e2..f68c01b18 100644
--- a/plugins/decl_mode/decl_interp.ml
+++ b/plugins/decl_mode/decl_interp.ml
@@ -91,7 +91,7 @@ let rec add_vars_of_simple_pattern globs = function
(UserError ("simple_pattern",str "\"as\" is not allowed here"))*)
| CPatOr (loc, _)->
Loc.raise ~loc
- (UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
+ (UserError (Some "simple_pattern",str "\"(_ | _)\" is not allowed here"))
| CPatDelimiters (_,_,p) ->
add_vars_of_simple_pattern globs p
| CPatCstr (_,_,pl1,pl2) ->
@@ -328,7 +328,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
let _ =
let expected = mib.Declarations.mind_nparams - num_params in
if not (Int.equal (List.length params) expected) then
- user_err "suppose it is"
+ user_err ~hdr:"suppose it is"
(str "Wrong number of extra arguments: " ++
(if Int.equal expected 0 then str "none" else int expected) ++ spc () ++
str "expected.") in
@@ -348,7 +348,7 @@ let interp_cases info env sigma params (pat:cases_pattern_expr) hyps =
Thesis (Plain) -> Glob_term.GSort(Loc.ghost,GProp)
| Thesis (For rec_occ) ->
if not (Id.List.mem rec_occ pat_vars) then
- user_err "suppose it is"
+ user_err ~hdr:"suppose it is"
(str "Variable " ++ Nameops.pr_id rec_occ ++
str " does not occur in pattern.");
Glob_term.GSort(Loc.ghost,GProp)