diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index aa795106a..9dcb5d2a5 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -204,7 +204,7 @@ let error_instantiate_pattern id l = | [_] -> "is" | _ -> "are" in - user_err "" (str "Cannot substitute the term bound to " ++ pr_id id + user_err (str "Cannot substitute the term bound to " ++ pr_id id ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l ++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.") @@ -315,7 +315,7 @@ let rec subst_pattern subst pat = let mkPLambda na b = PLambda(na,PMeta None,b) let rev_it_mkPLambda = List.fold_right mkPLambda -let err ?loc pp = user_err ?loc "pattern_of_glob_constr" pp +let err ?loc pp = user_err ?loc ~hdr:"pattern_of_glob_constr" pp let warn_cast_in_pattern = CWarnings.create ~name:"cast-in-pattern" ~category:"automation" @@ -387,7 +387,7 @@ let rec pat_of_raw metas vars = function rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p)) | (None | Some (GHole _)), _ -> PMeta None | Some p, None -> - user_err ~loc "" (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") + user_err ~loc (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.") in let info = { cip_style = sty; |