aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/g_romega.ml4
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega/g_romega.ml4')
-rw-r--r--plugins/romega/g_romega.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4
index fd4ede6c3..830dc54dd 100644
--- a/plugins/romega/g_romega.ml4
+++ b/plugins/romega/g_romega.ml4
@@ -27,7 +27,7 @@ let romega_tactic l =
| "positive" -> eval_tactic "zify_positive"
| "N" -> eval_tactic "zify_N"
| "Z" -> eval_tactic "zify_op"
- | s -> Errors.error ("No ROmega knowledge base for type "^s))
+ | s -> CErrors.error ("No ROmega knowledge base for type "^s))
(Util.List.sort_uniquize String.compare l)
in
Tacticals.New.tclTHEN