diff options
Diffstat (limited to 'ltac/tacentries.ml')
| -rw-r--r-- | ltac/tacentries.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ltac/tacentries.ml b/ltac/tacentries.ml index 1b7430c3f..2fed0e14f 100644 --- a/ltac/tacentries.ml +++ b/ltac/tacentries.ml @@ -429,7 +429,7 @@ let register_ltac local tacl = let kn = Lib.make_kn id in let id_pp = pr_id id in let () = if is_defined_tac kn then - CErrors.user_err ~loc "" + CErrors.user_err ~loc (str "There is already an Ltac named " ++ id_pp ++ str".") in let is_shadowed = @@ -446,7 +446,7 @@ let register_ltac local tacl = let kn = try Nametab.locate_tactic (snd (qualid_of_reference ident)) with Not_found -> - CErrors.user_err ~loc "" + CErrors.user_err ~loc (str "There is no Ltac named " ++ pr_reference ident ++ str ".") in UpdateTac kn, body |