diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 18:33:25 +0100 |
| commit | 1b92c226e563643da187b8614d5888dc4855eb43 (patch) | |
| tree | c4c3d204b36468b58cb71050ba95f06b8dd7bc2e /plugins/romega/const_omega.ml | |
| parent | 7c9b0a702976078b813e6493c1284af62a3f093c (diff) | |
Imported Upstream version 8.6
Diffstat (limited to 'plugins/romega/const_omega.ml')
| -rw-r--r-- | plugins/romega/const_omega.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 21b0f78b..4935fe4b 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.Id.to_string id) | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) | Term.Prod (Names.Name _,_,_),[] -> - Errors.error "Omega: Not a quantifier-free goal" + CErrors.error "Omega: Not a quantifier-free goal" | _ -> Kufo exception Destruct @@ -346,7 +346,7 @@ let parse_term t = | Kapp("Z.succ",[t]) -> Tsucc t | Kapp("Z.pred",[t]) -> Tplus(t, mk_Z (Bigint.neg Bigint.one)) | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> - (try Tnum (recognize t) with e when Errors.noncritical e -> Tother) + (try Tnum (recognize t) with e when CErrors.noncritical e -> Tother) | _ -> Tother with e when Logic.catchable_exception e -> Tother @@ -368,6 +368,6 @@ let is_scalar t = | Kapp(("Z.opp"|"Z.succ"|"Z.pred"),[t]) -> aux t | Kapp(("Zpos"|"Zneg"|"Z0"),_) -> let _ = recognize t in true | _ -> false in - try aux t with e when Errors.noncritical e -> false + try aux t with e when CErrors.noncritical e -> false end |