aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega/const_omega.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/romega/const_omega.ml')
-rw-r--r--plugins/romega/const_omega.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index e810e15c1..298b24850 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -39,7 +39,7 @@ let destructurate t =
| Term.Var id,[] -> Kvar(Names.string_of_id id)
| Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body)
| Term.Prod (Names.Name _,_,_),[] ->
- Util.error "Omega: Not a quantifier-free goal"
+ Errors.error "Omega: Not a quantifier-free goal"
| _ -> Kufo
exception Destruct