aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/omega/g_omega.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/omega/g_omega.ml4')
-rw-r--r--plugins/omega/g_omega.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index 6b711a176..ce7ffb1e7 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.ml4
@@ -35,7 +35,7 @@ let omega_tactic l =
| "positive" -> eval_tactic "zify_positive"
| "N" -> eval_tactic "zify_N"
| "Z" -> eval_tactic "zify_op"
- | s -> CErrors.error ("No Omega knowledge base for type "^s))
+ | s -> CErrors.user_err Pp.(str ("No Omega knowledge base for type "^s)))
(Util.List.sort_uniquize String.compare l)
in
Tacticals.New.tclTHEN