Compiles with both versions of Coq

1 files changed, 37 insertions, 37 deletions

diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 07064bb..589d59a 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -21,8 +21,8 @@ open Declare
 open Decl_kinds
 open Entries
 open Util
-(* open Micromega *)
-(* open Coq_micromega *)
+open Structures.Micromega_plugin_Micromega
+open Structures.Micromega_plugin_Coq_micromega
 
 open SmtMisc
 open SmtForm
@@ -32,19 +32,19 @@ open SmtAtom
 
 let rec pos_of_int i =
   if i <= 1
-  then Micromega_plugin.Micromega.XH
+  then XH
   else
     if i land 1 = 0
-    then Micromega_plugin.Micromega.XO(pos_of_int (i lsr 1))
-    else Micromega_plugin.Micromega.XI(pos_of_int (i lsr 1))
+    then XO(pos_of_int (i lsr 1))
+    else XI(pos_of_int (i lsr 1))
 
 let z_of_int i =
   if i = 0
-  then Micromega_plugin.Micromega.Z0
+  then Z0
   else
     if i > 0
-    then Micromega_plugin.Micromega.Zpos (pos_of_int i)
-    else Micromega_plugin.Micromega.Zneg (pos_of_int (-i))
+    then Zpos (pos_of_int i)
+    else Zneg (pos_of_int (-i))
 
 type my_tbl =
     {tbl:(hatom,int) Hashtbl.t; mutable count:int}
@@ -62,19 +62,19 @@ let create_tbl n = {tbl=Hashtbl.create n;count=1}
 let rec smt_Atom_to_micromega_pos ha =
   match Atom.atom ha with
   | Auop(UO_xO, ha) ->
-      Micromega_plugin.Micromega.XO (smt_Atom_to_micromega_pos ha)
+      XO (smt_Atom_to_micromega_pos ha)
   | Auop(UO_xI, ha) ->
-      Micromega_plugin.Micromega.XI (smt_Atom_to_micromega_pos ha)
-  | Acop CO_xH -> Micromega_plugin.Micromega.XH
+      XI (smt_Atom_to_micromega_pos ha)
+  | Acop CO_xH -> XH
   | _ -> raise Not_found
 
 let smt_Atom_to_micromega_Z ha =
   match Atom.atom ha with
   | Auop(UO_Zpos, ha) ->
-      Micromega_plugin.Micromega.Zpos (smt_Atom_to_micromega_pos ha)
+      Zpos (smt_Atom_to_micromega_pos ha)
   | Auop(UO_Zneg, ha) ->
-      Micromega_plugin.Micromega.Zneg (smt_Atom_to_micromega_pos ha)
-  | Acop CO_Z0 -> Micromega_plugin.Micromega.Z0
+      Zneg (smt_Atom_to_micromega_pos ha)
+  | Acop CO_Z0 -> Z0
   | _ -> raise Not_found
 
 let rec smt_Atom_to_micromega_pExpr tbl ha =
@@ -82,23 +82,23 @@ let rec smt_Atom_to_micromega_pExpr tbl ha =
   | Abop (BO_Zplus, ha, hb) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
       let b = smt_Atom_to_micromega_pExpr tbl hb in
-      Micromega_plugin.Micromega.PEadd(a, b)
+      PEadd(a, b)
   | Abop (BO_Zmult, ha, hb) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
       let b = smt_Atom_to_micromega_pExpr tbl hb in
-      Micromega_plugin.Micromega.PEmul(a, b)
+      PEmul(a, b)
   | Abop (BO_Zminus, ha, hb) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
       let b = smt_Atom_to_micromega_pExpr tbl hb in
-      Micromega_plugin.Micromega.PEsub(a, b)
+      PEsub(a, b)
   | Auop (UO_Zopp, ha) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
-      Micromega_plugin.Micromega.PEopp a
+      PEopp a
   | _ ->
-      try Micromega_plugin.Micromega.PEc (smt_Atom_to_micromega_Z ha)
+      try PEc (smt_Atom_to_micromega_Z ha)
       with Not_found ->
 	let v = get_atom_var tbl ha in
-	Micromega_plugin.Micromega.PEX (pos_of_int v)
+	PEX (pos_of_int v)
 
 
 (* morphism for LIA proposition (=, >, ...) *)
@@ -106,17 +106,17 @@ let rec smt_Atom_to_micromega_pExpr tbl ha =
 let smt_binop_to_micromega_formula tbl op ha hb =
   let op =
     match op with
-    | BO_Zlt -> Micromega_plugin.Micromega.OpLt
-    | BO_Zle -> Micromega_plugin.Micromega.OpLe
-    | BO_Zge -> Micromega_plugin.Micromega.OpGe
-    | BO_Zgt -> Micromega_plugin.Micromega.OpGt
-    | BO_eq _ -> Micromega_plugin.Micromega.OpEq
+    | BO_Zlt -> OpLt
+    | BO_Zle -> OpLe
+    | BO_Zge -> OpGe
+    | BO_Zgt -> OpGt
+    | BO_eq _ -> OpEq
     | _ -> Structures.error
 	  "lia.ml: smt_binop_to_micromega_formula expecting a formula"
   in
   let lhs = smt_Atom_to_micromega_pExpr tbl ha in
   let rhs = smt_Atom_to_micromega_pExpr tbl hb in
-  {Micromega_plugin.Micromega.flhs = lhs; Micromega_plugin.Micromega.fop = op; Micromega_plugin.Micromega.frhs = rhs }
+  {flhs = lhs; fop = op; frhs = rhs }
 
 let rec smt_Atom_to_micromega_formula tbl ha =
   match Atom.atom ha with
@@ -127,7 +127,7 @@ let rec smt_Atom_to_micromega_formula tbl ha =
 (* specialized fold *)
 
 let default_constr = mkInt 0
-let default_tag = Micromega_plugin.Mutils.Tag.from 0
+let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0
 (* morphism for general formulas *)
 
 let binop_array g tbl op def t =
@@ -145,14 +145,14 @@ let rec smt_Form_to_coq_micromega_formula tbl l =
   let v =
     match Form.pform l with
       | Fatom ha ->
-	Micromega_plugin.Coq_micromega.A (smt_Atom_to_micromega_formula tbl ha,
+	A (smt_Atom_to_micromega_formula tbl ha,
 	   default_tag,default_constr)
-      | Fapp (Ftrue, _) -> Micromega_plugin.Coq_micromega.TT
-      | Fapp (Ffalse, _) -> Micromega_plugin.Coq_micromega.FF
-      | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.C (x,y)) Micromega_plugin.Coq_micromega.TT l
-      | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.D (x,y)) Micromega_plugin.Coq_micromega.FF l
+      | Fapp (Ftrue, _) -> TT
+      | Fapp (Ffalse, _) -> FF
+      | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> C (x,y)) TT l
+      | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> D (x,y)) FF l
       | Fapp (Fxor, l) -> failwith "todo:Fxor"
-      | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.I (x,None,y)) Micromega_plugin.Coq_micromega.TT l
+      | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> I (x,None,y)) TT l
       | Fapp (Fiff, l) -> failwith "todo:Fiff"
       | Fapp (Fite, l) -> failwith "todo:Fite"
       | Fapp (Fnot2 _, l) ->
@@ -162,7 +162,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l =
           smt_Form_to_coq_micromega_formula tbl l.(0)
   in
   if Form.is_pos l then v
-  else Micromega_plugin.Coq_micromega.N(v)
+  else N(v)
 
 let binop_list tbl op def l =
   match l with
@@ -198,11 +198,11 @@ let binop_list tbl op def l =
 
 
 let smt_clause_to_coq_micromega_formula tbl cl =
-  binop_list tbl (fun x y -> Micromega_plugin.Coq_micromega.C(x,y)) Micromega_plugin.Coq_micromega.TT (List.map Form.neg cl)
+  binop_list tbl (fun x y -> C(x,y)) TT (List.map Form.neg cl)
 
 (* call to micromega solver *)
 let build_lia_certif cl =
   let tbl = create_tbl 13 in
-  let f = Micromega_plugin.Coq_micromega.I(smt_clause_to_coq_micromega_formula tbl cl, None, Micromega_plugin.Coq_micromega.FF) in
-  tbl, f, Micromega_plugin.Coq_micromega.tauto_lia f
+  let f = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in
+  tbl, f, tauto_lia f