diff options
Diffstat (limited to 'ltac/tacintern.ml')
| -rw-r--r-- | ltac/tacintern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index dc216da11..a1d34b53f 100644 --- a/ltac/tacintern.ml +++ b/ltac/tacintern.ml @@ -748,7 +748,7 @@ let print_ltac id = ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined with Not_found -> - errorlabstrm "print_ltac" + user_err "print_ltac" (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") (** Registering *) |