diff options
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 1 | ||||
| -rw-r--r-- | plugins/omega/g_omega.ml4 | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index d7dfe1491d..1057c646f8 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -13,6 +13,7 @@ (* *) (**************************************************************************) +open Errors open Util open Pp open Reduction diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 84cc8464f9..4aad8e7383 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -25,7 +25,7 @@ let omega_tactic l = | "positive" -> Tacinterp.interp <:tactic<zify_positive>> | "N" -> Tacinterp.interp <:tactic<zify_N>> | "Z" -> Tacinterp.interp <:tactic<zify_op>> - | s -> Util.error ("No Omega knowledge base for type "^s)) + | s -> Errors.error ("No Omega knowledge base for type "^s)) (Util.list_uniquize (List.sort compare l)) in tclTHEN |