From 20831b39a73ebd38336f19ad4ddb4d6b1078d60d Mon Sep 17 00:00:00 2001 From: Chantal Keller Date: Tue, 31 Mar 2020 20:25:05 +0200 Subject: Compiles with Coq-8.10 --- src/QInst.v | 2 +- src/lfsc/ast.ml | 4 +- src/lfsc/builtin.ml | 2 +- src/lfsc/shashcons.mli | 2 + src/lia/lia.ml | 223 +++++++++++++++++++++++++++-------- src/lia/lia.mli | 54 --------- src/smtlib2/smtlib2_genConstr.ml | 2 +- src/trace/smtCommands.ml | 2 +- src/verit/veritSyntax.ml | 4 +- src/versions/standard/structures.ml | 1 + src/versions/standard/structures.mli | 1 + 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 -- cgit