diff options
Diffstat (limited to 'ltac/tacenv.ml')
| -rw-r--r-- | ltac/tacenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/tacenv.ml b/ltac/tacenv.ml index c709ab114..5808feeba 100644 --- a/ltac/tacenv.ml +++ b/ltac/tacenv.ml @@ -65,7 +65,7 @@ let interp_ml_tactic { mltac_name = s; mltac_index = i } = let () = if Array.length tacs <= i then raise Not_found in tacs.(i) with Not_found -> - CErrors.errorlabstrm "" + CErrors.user_err "" (str "The tactic " ++ pr_tacname s ++ str " is not installed.") (***************************************************************************) |