Compiles with Coq-8.10

11 files changed, 184 insertions, 113 deletions

diff --git a/src/QInst.v b/src/QInst.v
index 611973e..cb533ee 100644
--- a/src/QInst.v
+++ b/src/QInst.v
@@ -69,7 +69,7 @@ Ltac vauto :=
          eapply impl_or_split_left; apply H
        end;
        apply H);
-  auto.
+  auto with smtcoq_core.
 
 
 
diff --git a/src/lfsc/ast.ml b/src/lfsc/ast.ml
index 454bc0a..36c2f79 100644
--- a/src/lfsc/ast.ml
+++ b/src/lfsc/ast.ml
@@ -198,7 +198,7 @@ let compare_symbol s1 s2 = match s1.sname, s2.sname with
   | Name n1, Name n2 -> Hstring.compare n1 n2
   | Name _, _ -> -1
   | _, Name _ -> 1
-  | S_Hole i1, S_Hole i2 -> Pervasives.compare i1 i2
+  | S_Hole i1, S_Hole i2 -> Stdlib.compare i1 i2
 
 
 let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with
@@ -250,7 +250,7 @@ let rec compare_term ?(mod_eq=false) t1 t2 = match t1.value, t2.value with
   | SideCond (_, _, _, t), _ -> compare_term ~mod_eq t t2
   | _, SideCond (_, _, _, t) -> compare_term ~mod_eq t1 t
 
-  | Hole i1, Hole i2 -> Pervasives.compare i1 i2
+  | Hole i1, Hole i2 -> Stdlib.compare i1 i2
 
 
 and compare_term_list ?(mod_eq=false) l1 l2 = match l1, l2 with
diff --git a/src/lfsc/builtin.ml b/src/lfsc/builtin.ml
index 86899df..75ea11e 100644
--- a/src/lfsc/builtin.ml
+++ b/src/lfsc/builtin.ml
@@ -616,7 +616,7 @@ let cong s1 s2 a1 b1 a2 b2 u1 u2 =
 
 module MInt = Map.Make (struct
     type t = int
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end)
 
 module STerm = Set.Make (Term)
diff --git a/src/lfsc/shashcons.mli b/src/lfsc/shashcons.mli
index 049ec5f..ca46efa 100644
--- a/src/lfsc/shashcons.mli
+++ b/src/lfsc/shashcons.mli
@@ -47,6 +47,7 @@ module type S =
 
     val iter : (t -> unit) -> unit
       (** [iter f] iterates [f] over all elements of the table . *)
+
     val stats : unit -> int * int * int * int * int * int
       (** Return statistics on the table.  The numbers are, in order:
 	  table length, number of entries, sum of bucket lengths,
@@ -83,6 +84,7 @@ module type S_consed =
 
     val iter : (key hash_consed -> unit) -> unit
       (** [iter f] iterates [f] over all elements of the table . *)
+
     val stats : unit -> int * int * int * int * int * int
       (** Return statistics on the table.  The numbers are, in order:
 	  table length, number of entries, sum of bucket lengths,
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index d546559..8dce3e8 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -13,9 +13,7 @@
 (*** Linking SMT Terms to Micromega Terms ***)
 open Util
 open Structures.Micromega_plugin_Micromega
-open Structures.Micromega_plugin_Coq_micromega
 
-open SmtMisc
 open SmtForm
 open SmtAtom
 
@@ -29,14 +27,6 @@ let rec pos_of_int i =
     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 Z0
-  else
-    if i > 0
-    then Zpos (pos_of_int i)
-    else Zneg (pos_of_int (-i))
-
 type my_tbl =
     {tbl:(hatom,int) Hashtbl.t; mutable count:int}
 
@@ -117,8 +107,6 @@ let smt_Atom_to_micromega_formula tbl ha =
 
 (* specialized fold *)
 
-let default_constr = Structures.econstr_of_constr (mkInt 0)
-let default_tag = Structures.Micromega_plugin_Mutils.Tag.from 0
 (* morphism for general formulas *)
 
 let binop_array g tbl op def t =
@@ -135,12 +123,10 @@ let binop_array g tbl op def t =
 let rec smt_Form_to_coq_micromega_formula tbl l =
   let v =
     match Form.pform l with
-      | Fatom ha ->
-	A (smt_Atom_to_micromega_formula tbl ha,
-	   default_tag,default_constr)
+      | Fatom ha -> A (smt_Atom_to_micromega_formula tbl ha, Tt)
       | 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 (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Cj (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 -> I (x,None,y)) TT l
@@ -162,49 +148,184 @@ let binop_list tbl op def l =
   | [] -> def
   | f::l -> List.fold_left (fun x y -> op x (smt_Form_to_coq_micromega_formula tbl y)) (smt_Form_to_coq_micromega_formula tbl f) l
 
+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 rec binop_list tbl op def l = *)
-(*   match l with *)
-(*   | [] -> def *)
-(*   | [f] -> smt_Form_to_coq_micromega_formula tbl f *)
-(*   | f::l -> *)
-(*       op (smt_Form_to_coq_micromega_formula tbl f) (binop_list tbl op def l) *)
-
-(* and smt_Form_to_coq_micromega_formula tbl l = *)
-(*   let v = *)
-(*     match Form.pform l with *)
-(*       | Fatom ha -> *)
-(* 	A (smt_Atom_to_micromega_formula tbl ha, *)
-(* 	   default_tag,default_constr) *)
-(*       | Fapp (Ftrue, _) -> TT *)
-(*       | Fapp (Ffalse, _) -> FF *)
-(*       | Fapp (Fand, l) -> binop_list tbl (fun x y -> C (x,y)) TT l *)
-(*       | Fapp (For, l) -> binop_list tbl (fun x y -> D (x,y)) FF l *)
-(*       | Fapp (Fxor, l) -> failwith "todo:Fxor" *)
-(*       | Fapp (Fimp, l) -> binop_list 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) -> smt_Form_to_coq_micromega_formula tbl l *)
-(*   in *)
-(*   if Form.is_pos l then v *)
-(*   else N(v) *)
 
+(* backported from Coq *)
+type ('option,'a,'prf,'model) prover = {
+  name : string ; (* name of the prover *)
+  get_option : unit ->'option ; (* find the options of the prover *)
+  prover : ('option *  'a list) -> ('prf, 'model) Structures.Micromega_plugin_Certificate.res ; (* the prover itself *)
+  hyps : 'prf -> Structures.Micromega_plugin_Mutils.ISet.t ; (* extract the indexes of the hypotheses really used in the proof *)
+  compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *)
+  pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *)
+  pp_f   : out_channel -> 'a   -> unit (* pretty printing of the formulas (polynomials)*)
+}
 
-let smt_clause_to_coq_micromega_formula tbl cl =
-  binop_list tbl (fun x y -> C(x,y)) TT (List.map Form.neg cl)
+let lia_enum  = ref true
+let max_depth = max_int
+let lia_proof_depth = ref max_depth
+let get_lia_option () =
+ (!Structures.Micromega_plugin_Certificate.use_simplex,!lia_enum,!lia_proof_depth)
+
+let lift_pexpr_prover p l =  p (List.map (fun (e,o) -> Structures.Micromega_plugin_Micromega.denorm e , o) l)
+
+module CacheZ = Structures.Micromega_plugin_Persistent_cache.PHashtable(struct
+ type prover_option = bool * bool* int
+ type t = prover_option * ((Structures.Micromega_plugin_Micromega.z Structures.Micromega_plugin_Micromega.pol * Structures.Micromega_plugin_Micromega.op1) list)
+  let equal = (=)
+  let hash  = Hashtbl.hash
+end)
+
+let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((_,ce,b),s) -> lift_pexpr_prover (Structures.Micromega_plugin_Certificate.lia ce b) s)
+
+let xhyps_of_cone base acc prf =
+  let rec xtract e acc =
+    match e with
+    | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> acc
+    | Structures.Micromega_plugin_Micromega.PsatzIn n -> let n = (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n) in
+                        if n >= base
+                        then  Structures.Micromega_plugin_Mutils.ISet.add (n-base) acc
+                        else acc
+    | Structures.Micromega_plugin_Micromega.PsatzMulC(_,c) -> xtract  c acc
+    | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) |  Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in
+
+    xtract prf acc
+
+let hyps_of_pt pt =
+
+  let rec xhyps base pt acc =
+    match pt with
+      | Structures.Micromega_plugin_Micromega.DoneProof -> acc
+      | Structures.Micromega_plugin_Micromega.RatProof(c,pt) ->  xhyps (base+1) pt (xhyps_of_cone base acc c)
+      | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
+      | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) ->
+          let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
+            List.fold_left (fun s x -> xhyps (base + 1) x s) s l in
+
+    xhyps 0 pt Structures.Micromega_plugin_Mutils.ISet.empty
+
+let compact_cone prf f  =
+  let np n = Structures.Micromega_plugin_Mutils.CamlToCoq.nat (f (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)) in
+
+  let rec xinterp prf =
+    match prf with
+    | Structures.Micromega_plugin_Micromega.PsatzC _ | Structures.Micromega_plugin_Micromega.PsatzZ | Structures.Micromega_plugin_Micromega.PsatzSquare _ -> prf
+    | Structures.Micromega_plugin_Micromega.PsatzIn n -> Structures.Micromega_plugin_Micromega.PsatzIn (np n)
+    | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) -> Structures.Micromega_plugin_Micromega.PsatzMulC(e,xinterp c)
+    | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzAdd(xinterp e1,xinterp e2)
+    | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) -> Structures.Micromega_plugin_Micromega.PsatzMulE(xinterp e1,xinterp e2) in
+
+    xinterp prf
+
+let compact_pt pt f =
+  let translate ofset x =
+    if x < ofset then x
+    else (f (x-ofset) + ofset) in
+
+  let rec compact_pt ofset pt =
+    match pt with
+      | Structures.Micromega_plugin_Micromega.DoneProof -> Structures.Micromega_plugin_Micromega.DoneProof
+      | Structures.Micromega_plugin_Micromega.RatProof(c,pt) -> Structures.Micromega_plugin_Micromega.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
+      | Structures.Micromega_plugin_Micromega.CutProof(c,pt) -> Structures.Micromega_plugin_Micromega.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
+      | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,l) -> Structures.Micromega_plugin_Micromega.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)),
+                                                   Structures.Micromega_plugin_Micromega.map (fun x -> compact_pt (ofset+1) x) l) in
+    compact_pt 0 pt
+
+let pp_nat o n = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.nat n)
+
+let pp_positive o x = Printf.fprintf o "%i" (Structures.Micromega_plugin_Mutils.CoqToCaml.positive x)
+
+let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (Structures.Micromega_plugin_Mutils.CoqToCaml.z_big_int x))
+
+let pp_list op cl elt o l =
+  let rec _pp  o l =
+    match l with
+      | [] -> ()
+      | [e] -> Printf.fprintf o "%a" elt e
+      | e::l -> Printf.fprintf o "%a ,%a" elt e  _pp l in
+  Printf.fprintf o "%s%a%s" op _pp l cl
+
+let pp_pol pp_c o e =
+  let rec pp_pol o e =
+    match e with
+      | Structures.Micromega_plugin_Micromega.Pc n -> Printf.fprintf o "Pc %a" pp_c n
+      | Structures.Micromega_plugin_Micromega.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
+      | Structures.Micromega_plugin_Micromega.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
+  pp_pol o e
+
+let pp_psatz pp_z o e =
+  let rec pp_cone o e =
+    match e with
+      | Structures.Micromega_plugin_Micromega.PsatzIn n ->
+         Printf.fprintf o "(In %a)%%nat" pp_nat n
+      | Structures.Micromega_plugin_Micromega.PsatzMulC(e,c) ->
+         Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
+      | Structures.Micromega_plugin_Micromega.PsatzSquare e ->
+         Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
+      | Structures.Micromega_plugin_Micromega.PsatzAdd(e1,e2) ->
+         Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
+      | Structures.Micromega_plugin_Micromega.PsatzMulE(e1,e2) ->
+         Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
+      | Structures.Micromega_plugin_Micromega.PsatzC p ->
+         Printf.fprintf o "(%a)%%positive" pp_z p
+      | Structures.Micromega_plugin_Micromega.PsatzZ    ->
+         Printf.fprintf o "0" in
+  pp_cone o e
+
+let rec pp_proof_term o = function
+  | Structures.Micromega_plugin_Micromega.DoneProof -> Printf.fprintf o "D"
+  | Structures.Micromega_plugin_Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+  | Structures.Micromega_plugin_Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz pp_z) cone pp_proof_term rst
+  | Structures.Micromega_plugin_Micromega.EnumProof(c1,c2,rst) ->
+      Printf.fprintf o "EP[%a,%a,%a]"
+        (pp_psatz pp_z) c1 (pp_psatz pp_z) c2
+     (pp_list "[" "]" pp_proof_term) rst
+
+let linear_Z =   {
+  name    = "lia";
+ get_option = get_lia_option;
+ prover  = memo_zlinear_prover ;
+  hyps    = hyps_of_pt;
+  compact = compact_pt;
+  pp_prf  = pp_proof_term;
+  pp_f    = fun o x -> pp_pol pp_z o (fst x)
+}
+
+let find_witness  p polys1 =
+  let polys1 = List.map fst polys1 in
+  match p.prover (p.get_option (), polys1) with
+  | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model m
+  | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown
+  | Structures.Micromega_plugin_Certificate.Prf prf -> Structures.Micromega_plugin_Certificate.Prf(prf,p)
+
+let witness_list prover l =
+ let rec xwitness_list l =
+  match l with
+   | [] -> Structures.Micromega_plugin_Certificate.Prf []
+   | e :: l ->
+      match xwitness_list l with
+      | Structures.Micromega_plugin_Certificate.Model (m,e) -> Structures.Micromega_plugin_Certificate.Model (m,e)
+      | Structures.Micromega_plugin_Certificate.Unknown     -> Structures.Micromega_plugin_Certificate.Unknown
+      | Structures.Micromega_plugin_Certificate.Prf l ->
+         match find_witness  prover e  with
+         | Structures.Micromega_plugin_Certificate.Model m -> Structures.Micromega_plugin_Certificate.Model (m,e)
+         | Structures.Micromega_plugin_Certificate.Unknown -> Structures.Micromega_plugin_Certificate.Unknown
+         | Structures.Micromega_plugin_Certificate.Prf w ->  Structures.Micromega_plugin_Certificate.Prf (w::l) in
+ xwitness_list l
+
+let witness_list_tags = witness_list
 
-(* backported from Coq-8.8.2 *)
-(* val tauto_lia : Mc.z formula -> Certificate.Mc.zArithProof list option *)
 let tauto_lia ff =
   let prover = linear_Z in
-  let cnf_ff,_ = cnf Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce  ff in
-  match witness_list_tags [prover] cnf_ff with
-    | None -> None
-    | Some l -> Some (List.map fst l)
+  let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in
+  match witness_list_tags prover cnf_ff with
+    | Structures.Micromega_plugin_Certificate.Prf l -> Some (List.map fst l)
+    | _ -> None
 
 (* call to micromega solver *)
 let build_lia_certif cl =
   let tbl = create_tbl 13 in
   let f = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in
-  tbl, f, tauto_lia f
-
+  tauto_lia f
diff --git a/src/lia/lia.mli b/src/lia/lia.mli
index 9d4ee6b..fb58db8 100644
--- a/src/lia/lia.mli
+++ b/src/lia/lia.mli
@@ -10,60 +10,6 @@
 (**************************************************************************)
 
 
-val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive
-val z_of_int : int -> Structures.Micromega_plugin_Micromega.z
-type my_tbl
-val get_atom_var : my_tbl -> SmtAtom.hatom -> int
-val create_tbl : int -> my_tbl
-val smt_Atom_to_micromega_pos :
-  SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.positive
-val smt_Atom_to_micromega_Z :
-  SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.z
-val smt_Atom_to_micromega_pExpr :
-  my_tbl ->
-  SmtAtom.hatom ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Micromega.pExpr
-val smt_binop_to_micromega_formula :
-  my_tbl ->
-  SmtAtom.bop ->
-  SmtAtom.hatom ->
-  SmtAtom.hatom ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Micromega.formula
-val smt_Atom_to_micromega_formula :
-  my_tbl ->
-  SmtAtom.hatom ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Micromega.formula
-val binop_array :
-  ('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c
-val smt_Form_to_coq_micromega_formula :
-  my_tbl ->
-  SmtAtom.Form.t ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Coq_micromega.formula
-val binop_list :
-  my_tbl ->
-  (Structures.Micromega_plugin_Micromega.z
-   Structures.Micromega_plugin_Coq_micromega.formula ->
-   Structures.Micromega_plugin_Micromega.z
-   Structures.Micromega_plugin_Coq_micromega.formula ->
-   Structures.Micromega_plugin_Micromega.z
-   Structures.Micromega_plugin_Coq_micromega.formula) ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Coq_micromega.formula ->
-  SmtAtom.Form.t list ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Coq_micromega.formula
-val smt_clause_to_coq_micromega_formula :
-  my_tbl ->
-  SmtAtom.Form.t list ->
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Coq_micromega.formula
 val build_lia_certif :
   SmtAtom.Form.t list ->
-  my_tbl *
-  Structures.Micromega_plugin_Micromega.z
-  Structures.Micromega_plugin_Coq_micromega.formula *
   Structures.Micromega_plugin_Certificate.Mc.zArithProof list option
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index f938671..7e58aa3 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -111,7 +111,7 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
 
 let declare_fun_from_name rt ro s tyl ty =
   let coqTy = List.fold_right (fun typ c ->
-      Term.mkArrow (interp_to_coq rt typ) c)
+      Structures.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
   let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index e64a131..b1f2666 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) =
   let tf = Hashtbl.create 17 in
   let rec interp = function
     | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
-    | c::prem -> Term.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
+    | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
   interp prem
 
 
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index b1a6304..862a628 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -150,7 +150,7 @@ let mkCongrPred p =
 (* Linear arithmetic *)
 
 let mkMicromega cl =
-  let _tbl, _f, cert = Lia.build_lia_certif cl in
+  let cert = Lia.build_lia_certif cl in
   let c =
     match cert with
     | None -> failwith "VeritSyntax.mkMicromega: micromega can't solve this"
@@ -168,7 +168,7 @@ let mkSplArith orig cl =
       match orig.value with
       | Some [orig'] -> orig'
       | _ -> failwith "VeritSyntax.mkSplArith: wrong number of literals in the premise clause" in
-    let _tbl, _f, cert = Lia.build_lia_certif [Form.neg orig';res] in
+    let cert = Lia.build_lia_certif [Form.neg orig';res] in
     let c =
       match cert with
       | None -> failwith "VeritSyntax.mkSplArith: micromega can't solve this"
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index becab90..3b112cf 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -173,6 +173,7 @@ module Micromega_plugin_Micromega = Micromega_plugin.Micromega
 module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
 module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
+module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache
 
 let micromega_coq_proofTerm =
   (* Cannot contain evars *)
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 1c4443e..950135c 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -93,6 +93,7 @@ module Micromega_plugin_Micromega = Micromega_plugin.Micromega
 module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
 module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
+module Micromega_plugin_Persistent_cache = Micromega_plugin.Persistent_cache
 
 val micromega_coq_proofTerm : constr lazy_t
 val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr