diff options
Diffstat (limited to 'plugins/romega/const_omega.ml')
-rw-r--r-- | plugins/romega/const_omega.ml | 2 |
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 |