diff options
Diffstat (limited to 'parsing/g_tactic.ml4')
| -rw-r--r-- | parsing/g_tactic.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 2cc2b01c0..3c2c45c72 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -136,7 +136,7 @@ let mk_fix_tac (loc,id,bl,ann,ty) = let mk_cofix_tac (loc,id,bl,ann,ty) = let _ = Option.map (fun (aloc,_) -> user_err ~loc:aloc - "Constr:mk_cofix_tac" + ~hdr:"Constr:mk_cofix_tac" (Pp.str"Annotation forbidden in cofix expression.")) ann in (id,CProdN(loc,bl,ty)) @@ -192,7 +192,7 @@ let merge_occurrences loc cl = function | None -> if Locusops.clause_with_generic_occurrences cl then (None, cl) else - user_err ~loc "" (str "Found an \"at\" clause without \"with\" clause.") + user_err ~loc (str "Found an \"at\" clause without \"with\" clause.") | Some (occs, p) -> let ans = match occs with | AllOccurrences -> cl @@ -204,9 +204,9 @@ let merge_occurrences loc cl = function { cl with onhyps = Some [(occs, id), l] } | _ -> if Locusops.clause_with_generic_occurrences cl then - user_err ~loc "" (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") + user_err ~loc (str "Unable to interpret the \"at\" clause; move it in the \"in\" clause.") else - user_err ~loc "" (str "Cannot use clause \"at\" twice.") + user_err ~loc (str "Cannot use clause \"at\" twice.") end in (Some p, ans) |