diff options
Diffstat (limited to 'src/lia')
-rw-r--r-- | src/lia/lia.ml | 13 | ||||
-rw-r--r-- | src/lia/lia.mli | 2 |
2 files changed, 7 insertions, 8 deletions
diff --git a/src/lia/lia.ml b/src/lia/lia.ml index 22b6ae0..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,8 +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 [] @@ -161,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 diff --git a/src/lia/lia.mli b/src/lia/lia.mli index 7b4c6c8..f996ac0 100644 --- a/src/lia/lia.mli +++ b/src/lia/lia.mli @@ -12,4 +12,4 @@ val build_lia_certif : SmtAtom.Form.t list -> - Structures.Micromega_plugin_Certificate.Mc.zArithProof list option + CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list option |