diff options
Diffstat (limited to 'src/lia/lia.ml')
| -rw-r--r-- | src/lia/lia.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 53dbf6d..e00092e 100644 --- a/src/lia/lia.ml +++ b/src/lia/lia.ml @@ -12,7 +12,7 @@ (*** Linking SMT Terms to Micromega Terms ***) open Util -open Structures.Micromega_plugin_Micromega +open CoqInterface.Micromega_plugin_Micromega open SmtForm open SmtAtom @@ -92,7 +92,7 @@ let smt_binop_to_micromega_formula tbl op ha hb = | BO_Zge -> OpGe | BO_Zgt -> OpGt | BO_eq _ -> OpEq - | _ -> Structures.error + | _ -> CoqInterface.error "lia.ml: smt_binop_to_micromega_formula expecting a formula" in let lhs = smt_Atom_to_micromega_pExpr tbl ha in @@ -102,7 +102,7 @@ let smt_binop_to_micromega_formula tbl op ha hb = let smt_Atom_to_micromega_formula tbl ha = match Atom.atom ha with | Abop (op,ha,hb) -> smt_binop_to_micromega_formula tbl op ha hb - | _ -> Structures.error + | _ -> CoqInterface.error "lia.ml: smt_Atom_to_micromega_formula was expecting an LIA formula" (* specialized fold *) @@ -152,7 +152,7 @@ let smt_clause_to_coq_micromega_formula tbl cl = binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl) let tauto_lia ff = - let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in + let cnf_ff,_ = CoqInterface.Micromega_plugin_Micromega.cnfZ ff in let rec xwitness_list l = match l with | [] -> Some [] @@ -160,8 +160,8 @@ let tauto_lia ff = match xwitness_list l with | None -> None | Some l -> - match Structures.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> Structures.Micromega_plugin_Micromega.denorm e, o) e) with - | Structures.Micromega_plugin_Certificate.Prf w -> Some (w::l) + match CoqInterface.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> CoqInterface.Micromega_plugin_Micromega.denorm e, o) e) with + | CoqInterface.Micromega_plugin_Certificate.Prf w -> Some (w::l) | _ -> None in xwitness_list cnf_ff |