diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-12-27 16:53:30 +0100 |
| commit | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (patch) | |
| tree | 26dd9c4aa142597ee09c887ef161d5f0fa5077b6 /plugins/romega/const_omega.ml | |
| parent | 164c6861860e6b52818c031f901ffeff91fca16a (diff) | |
Imported Upstream version 8.6upstream/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 |