diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 17ac7a4b6..5ba53a764 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -615,7 +615,8 @@ module New = struct | Var id -> string_of_id id | _ -> "\b" in - error ("The elimination combinator " ^ name_elim ^ " is unknown.") + errorlabstrm "Tacticals.general_elim_then_using" + (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain indmv elimclause indclause in let branchsigns = compute_construtor_signatures isrec ind in |