diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 28a7b634c..c9af1f11c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -643,7 +643,7 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - errorlabstrm "Tacticals.general_elim_then_using" + user_err "Tacticals.general_elim_then_using" (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in |