diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 99e54cad0af764e053ee1dafc7e361387e30b2e1..0c05374f3a184680de0625a57c77d8cbced021aa 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -1950,10 +1950,11 @@ struct
let rec lc_open m k v e =
if not (Bvars.contains k e.bind) then e else
match e.repr with
- | Bvar _ -> v
+ | Bvar _ -> v (* e.bind is a singleton that can only contains k *)
| _ ->
- try cache_find m e
- with Not_found -> cache_bind m e (rebuild (lc_open m k v) e)
+ if is_simple e then e else
+ try cache_find m e
+ with Not_found -> cache_bind m e (rebuild (lc_open m k v) e)
let lc_open_term t e =
let k = Bvars.order e.bind in
diff --git a/src/plugins/wp/Auto.mli b/src/plugins/wp/Auto.mli
index cd8447405dc1e8073b28c84f85b632c7592faa50..b91ae66a573fdf480367c2f5ba86429f9a2e6a83 100644
--- a/src/plugins/wp/Auto.mli
+++ b/src/plugins/wp/Auto.mli
@@ -35,7 +35,7 @@ val contrapose : ?priority:float -> selection -> strategy
val compound : ?priority:float -> selection -> strategy
val cut : ?priority:float -> ?modus:bool -> selection -> strategy
val filter : ?priority:float -> ?anti:bool -> unit -> strategy
-val havoc : ?priority:float -> havoc:selection -> addr:selection -> strategy
+val havoc : ?priority:float -> havoc:selection -> strategy
val separated : ?priority:float -> selection -> strategy
val instance : ?priority:float -> selection -> selection list -> strategy
val lemma : ?priority:float -> ?at:selection -> string -> selection list -> strategy
diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index 5b8539b2c9085ede840a8c805c957d1834529ab5..9264e1884c35c347282aaf8b07294a8f3fdb6a45 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -357,13 +357,13 @@ class pane (proverpane : GuiConfig.provers) =
printer#set_target Tactical.Empty ;
strategies#connect None ;
List.iter (fun tactic -> tactic#clear) tactics
- | Some(model,sequent,sel) ->
+ | Some(model,tree,sequent,sel) ->
strategies#connect (Some (self#strategies sequent)) ;
let select (tactic : GuiTactic.tactic) =
let process = self#apply in
let composer = self#compose in
let browser = self#browse in
- tactic#select ~process ~composer ~browser sel
+ tactic#select ~process ~composer ~browser ~tree sel
in
Model.with_model model (List.iter select) tactics ;
let tgt =
@@ -470,7 +470,7 @@ class pane (proverpane : GuiConfig.provers) =
let sequent = printer#sequent in
let select = printer#selection in
let model = wpo.Wpo.po_model in
- self#update_tactics (Some(model,sequent,select)) ;
+ self#update_tactics (Some(model,proof,sequent,select)) ;
end
| Composer _ | Browser _ -> ()
diff --git a/src/plugins/wp/GuiTactic.ml b/src/plugins/wp/GuiTactic.ml
index 40c8cf7256f05158a0364caaaad11889f2107349..a71c86bd8a48d1f81cbfc6e44352367def4e89a8 100644
--- a/src/plugins/wp/GuiTactic.ml
+++ b/src/plugins/wp/GuiTactic.ml
@@ -340,6 +340,7 @@ let wfield tac form pp = function
(* -------------------------------------------------------------------------- *)
type edited = {
+ tree : ProofEngine.tree ;
target : selection ;
browser : (browser -> unit) ;
composer : (composer -> unit) ;
@@ -388,6 +389,10 @@ class tactic
(* --- Feedback API --- *)
(* -------------------------------------------------------------------------- *)
+ method pool = match edited with
+ | None -> assert false
+ | Some { tree } -> ProofEngine.pool tree
+
method interactive = self#is_active
method get_title = title
method has_error = error
@@ -437,8 +442,8 @@ class tactic
method private updated () =
match edited with
| None -> ()
- | Some { process ; composer ; browser ; target } ->
- self#select ~process ~composer ~browser target
+ | Some { process ; composer ; browser ; target ; tree } ->
+ self#select ~process ~composer ~browser ~tree target
method clear =
begin
@@ -455,9 +460,11 @@ class tactic
try tac#select (self :> feedback) target
with Not_found | Exit -> Not_applicable
- method select ~process ~browser ~composer (target : selection) =
+ method select ~process ~browser ~composer ~tree
+ (target : selection) =
begin
self#reset_dongle ;
+ edited <- Some { process ; composer ; browser ; target ; tree } ;
let status = self#status target in
match status , error with
| Not_applicable , _ ->
@@ -466,12 +473,10 @@ class tactic
self#set_action () ;
| Not_configured , _ | Applicable _ , true ->
self#set_visible true ;
- edited <- Some { process ; composer ; browser ; target } ;
self#set_status `DIALOG_WARNING ;
self#set_action () ;
| Applicable proc , false ->
self#set_visible true ;
- edited <- Some { process ; composer ; browser ; target } ;
self#set_status `APPLY ;
let callback () = process tac target proc in
self#set_action ~callback () ;
diff --git a/src/plugins/wp/GuiTactic.mli b/src/plugins/wp/GuiTactic.mli
index 9d777188182b05a2fc6ef19a4c5d64de17b974af..40b9f2cc2320a3783ac0a6c5ddb1343137ffe308 100644
--- a/src/plugins/wp/GuiTactic.mli
+++ b/src/plugins/wp/GuiTactic.mli
@@ -64,6 +64,7 @@ class tactic : Tactical.t -> (Format.formatter -> Tactical.selection -> unit) ->
process:(tactical -> selection -> process -> unit) ->
browser:(browser -> unit) ->
composer:(composer -> unit) ->
+ tree:ProofEngine.tree ->
selection -> unit
end
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index fdcb24f90acfb8076919647c8c0e87985d746fff..8577ac6702ad80d543bdcdd3cd103aeee30db076 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -801,7 +801,9 @@ struct
else
match Context.get_opt context_pp with
| Some env -> Pretty.pp_term_env env fmt e
- | None -> Pretty.pp_term Pretty.empty fmt e
+ | None ->
+ let env = Pretty.known Pretty.empty (QED.vars e) in
+ Pretty.pp_term env fmt e
let pp_pred = pp_term
let pp_var fmt x = pp_term fmt (e_var x)
let pp_vars fmt xs =
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 6d2bca1144d0184eea2d63679675fa643615cccc..af909388a75859ce192afc8e84976e67c7c22711 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -40,6 +40,7 @@ and script =
type tree = {
main : Wpo.t ; (* Main goal to be proved. *)
+ mutable pool : Lang.F.pool option ; (* Global pool variable *)
mutable saved : bool ; (* Saved on Disk. *)
mutable gid : int ; (* WPO goal numbering *)
mutable head : node option ; (* the current node *)
@@ -53,6 +54,7 @@ module PROOFS = Model.StaticGenerator(Wpo.S)
let name = "Wp.ProofEngine.Proofs"
let compile main = {
main ; gid = 0 ;
+ pool = None ;
head = None ;
root = None ;
saved = false ;
@@ -73,6 +75,14 @@ let get wpo =
let iter_all f ns = List.iter (fun (_,n) -> f n) ns
let map_all f ns = List.map (fun (k,n) -> k,f n) ns
+let pool tree =
+ match tree.pool with
+ | Some pool -> pool
+ | None ->
+ let _,sequent = Wpo.compute tree.main in
+ let pool = Lang.new_pool ~vars:(Conditions.vars_seq sequent) () in
+ tree.pool <- Some pool ; pool
+
(* -------------------------------------------------------------------------- *)
(* --- Constructors --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 5d6e1f26afcc9628b824c27f09dea0659fce7bb8..78174d15cdf221a002c5b32a22ed8da79435290d 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -40,6 +40,7 @@ type state = [ `Opened | `Proved | `Pending of int | `Script of int ]
type current = [ `Main | `Internal of node | `Leaf of int * node ]
type position = [ `Main | `Node of node | `Leaf of int ]
+val pool : tree -> Lang.F.pool
val saved : tree -> bool
val set_saved : tree -> bool -> unit
diff --git a/src/plugins/wp/ProofScript.ml b/src/plugins/wp/ProofScript.ml
index 2f5b986d29a6a3c94ff0e8905df5e92eb10cd5ef..9bc0cf1931a1ea4d1942d60313099e0e3b65e683 100644
--- a/src/plugins/wp/ProofScript.ml
+++ b/src/plugins/wp/ProofScript.ml
@@ -429,11 +429,12 @@ let configure jtactic sequent =
(* --- Console --- *)
(* -------------------------------------------------------------------------- *)
-class console ~title =
+class console ~pool ~title =
object
val mutable the_title = title
+ method pool : Lang.F.pool = pool
method interactive = false
method get_title = the_title
method set_title : 'a. 'a formatter =
diff --git a/src/plugins/wp/ProofScript.mli b/src/plugins/wp/ProofScript.mli
index 3d82fbe6cada5d69e5eeeed88bff6889ffd1b59e..aca4732eea85763555c4597783ed0c00ec910921 100644
--- a/src/plugins/wp/ProofScript.mli
+++ b/src/plugins/wp/ProofScript.mli
@@ -23,7 +23,7 @@
open Tactical
open Conditions
-class console : title:string -> Tactical.feedback
+class console : pool:Lang.F.pool -> title:string -> Tactical.feedback
type jscript = alternative list
and alternative = private
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 199f8180f9e0678a76630cebc3c578bc76a4401c..6893ddb27814038b4a1516ab4657ce25218d71d4 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -78,7 +78,9 @@ let jconfigure (console : #Tactical.feedback) jtactic goal =
end
let jfork tree ?node jtactic =
- let console = new ProofScript.console ~title:jtactic.header in
+ let console = new ProofScript.console
+ ~pool:(ProofEngine.pool tree)
+ ~title:jtactic.header in
try
let anchor = ProofEngine.anchor tree ?node () in
let goal = ProofEngine.goal anchor in
diff --git a/src/plugins/wp/ProverSearch.ml b/src/plugins/wp/ProverSearch.ml
index d64e003cc1b4a06f50e3e9fe72c445f47aaa3036..cdd825cbe4aefaaf71992c28f4f1dbe917954e64 100644
--- a/src/plugins/wp/ProverSearch.ml
+++ b/src/plugins/wp/ProverSearch.ml
@@ -40,7 +40,9 @@ let configure (console : #Tactical.feedback) strategy =
| _ -> None
let fork tree anchor strategy =
- let console = new ProofScript.console ~title:strategy.tactical#title in
+ let console = new ProofScript.console
+ ~pool:(ProofEngine.pool tree)
+ ~title:strategy.tactical#title in
try
let model = ProofEngine.node_model anchor in
match Model.with_model model (configure console) strategy with
diff --git a/src/plugins/wp/TacCompound.ml b/src/plugins/wp/TacCompound.ml
index 09df4884d9a6f336b4fb2dcbaf03c87d402593bd..b1d5ec14505728c285c8de0e4b529d72fdfd7380 100644
--- a/src/plugins/wp/TacCompound.ml
+++ b/src/plugins/wp/TacCompound.ml
@@ -116,8 +116,7 @@ let field a b f =
Pretty_utils.sfprintf "Field %a" Lang.Field.pretty f ,
F.p_equal (F.e_getfield a f) (F.e_getfield b f)
-let index vars tau =
- let pool = Lang.new_pool ~vars () in
+let index ~pool tau =
let x = F.fresh pool tau in
[x] , F.e_var x
@@ -126,14 +125,14 @@ let neq i j p = F.p_imply (F.p_neq i j) p
let get1 a k v = F.p_equal (F.e_get a k) v
let get2 a b k = F.p_equal (F.e_get a k) (F.e_get b k)
-let clause ~(vars : F.Vars.t) = function
+let clause ~pool = function
| Record(a,b,fs) -> List.map (field a b) fs
| Array1((a,i,u),b,t) ->
- let ks,k = index vars t in
+ let ks,k = index ~pool t in
[ "Updated" , get1 b i u ;
"Others" , F.p_forall ks (neq i k (get2 a b k)) ]
| Array2((a,i,u),(b,j,v),t) ->
- let ks,k = index vars t in
+ let ks,k = index ~pool t in
[ "Updated (both)" , eq i j (F.p_equal u v) ;
"Updated (left)" , neq i j (get1 a j v) ;
"Updated (right)" , neq i j (get1 b i u) ;
@@ -153,47 +152,47 @@ let kind = function Record _ -> "compound" | Array1 _ | Array2 _ -> "array"
let equality eq = if eq then "equality" else "dis-equality"
let process_expand (feedback : Tactical.feedback) ?at e =
- let vars = F.vars e in
+ let pool = feedback#pool in
let eq,cmp = get_compound_equality e in
feedback#set_title "Compound (%s)" (name eq) ;
feedback#set_descr "Expand %s %s" (kind cmp) (equality eq) ;
- let e' = (if eq then conj else disj) (clause ~vars cmp) in
+ let e' = (if eq then conj else disj) (clause ~pool cmp) in
let cases = [feedback#get_title,F.p_true,e,F.e_prop e'] in
Tactical.rewrite ?at cases
let process_have (feedback : Tactical.feedback) s =
+ let pool = feedback#pool in
let e = F.e_prop (Conditions.have s) in
- let vars = F.vars e in
let eq,cmp = get_compound_equality e in
if eq then
begin
feedback#set_title "Compound (eq)" ;
feedback#set_descr "Expand %s equality" (kind cmp) ;
- let cases = ["Compound (eq)",When (conj (clause ~vars cmp))] in
+ let cases = ["Compound (eq)",When (conj (clause ~pool cmp))] in
Tactical.replace ~at:s.id cases
end
else
begin
feedback#set_title "Compound (split)" ;
feedback#set_descr "Split %s dis-equality" (kind cmp) ;
- let cases = List.map negative (clause ~vars cmp) in
+ let cases = List.map negative (clause ~pool cmp) in
Tactical.replace ~at:s.id cases
end
let process_goal (feedback : Tactical.feedback) p =
+ let pool = feedback#pool in
let eq,cmp = get_compound_equality (F.e_prop p) in
- let vars = F.varsp p in
if eq then
begin
feedback#set_title "Compound (split)" ;
feedback#set_descr "Split %s equality" (kind cmp) ;
- Tactical.split (clause ~vars cmp) ;
+ Tactical.split (clause ~pool cmp) ;
end
else
begin
feedback#set_title "Compound (neq)" ;
feedback#set_descr "Expand compound dis-equality" ;
- let cases = ["Compound (neq)",disj (clause ~vars cmp)] in
+ let cases = ["Compound (neq)",disj (clause ~pool cmp)] in
Tactical.split cases
end
diff --git a/src/plugins/wp/TacHavoc.ml b/src/plugins/wp/TacHavoc.ml
index ee2bbd7b4f0a68a8dc0ef47e36276d0cc8c58161..9b7034cc30839c0ed07020faf82927db93ef5e96 100644
--- a/src/plugins/wp/TacHavoc.ml
+++ b/src/plugins/wp/TacHavoc.ml
@@ -30,62 +30,38 @@ module L = Qed.Logic
(* --- Havoc --- *)
(* -------------------------------------------------------------------------- *)
-let field,parameter =
- Tactical.composer
- ~id:"address"
- ~title:"Address"
- ~descr:"Access Outside the Assigned Range"
- ()
-
-let has_type t e =
- try F.Tau.equal t (F.typeof e)
- with Not_found -> false
-
-let match_havoc =
- let havoc m1 = function
- | L.Fun( f , [m_undef;m0;a;n] ) when f == MemTyped.f_havoc -> m1,(m_undef,m0,a,n)
- | _ -> raise Not_found
- in function
- | L.Eq (m,m') -> (try havoc m' (F.repr m) with | Not_found -> havoc m (F.repr m'))
- | _ -> raise Not_found
+let lookup_havoc e =
+ match F.repr e with
+ | L.Aget( m , p ) ->
+ begin
+ match F.repr m with
+ | L.Fun( f , [mr;m0;a;n] ) when f == MemTyped.f_havoc ->
+ Some( mr , m0 , a , n , p )
+ | _ -> None
+ end
+ | _ -> None
class havoc =
- object(self)
+ object
inherit Tactical.make ~id:"Wp.havoc"
~title:"Havoc"
~descr:"Go Through Assigns"
- ~params:[parameter]
+ ~params:[]
- method select feedback sel =
- match sel with
- | Clause(Step s) ->
- begin
- match s.condition with
- | Have p | When p ->
- let m1,(m_undef,m0,a,n) = match_havoc (F.e_expr p) in
- let tp = F.typeof a in
- feedback#update_field ~filter:(has_type tp) field ;
- let sel = self#get_field field in
- if not (Tactical.is_empty sel) then
- let ptr = Tactical.selected sel in
- if has_type tp ptr then
- let separated =
- F.p_call MemTyped.p_separated
- [ ptr ; F.e_int 1 ; a ; n ] in
- let equal_unassigned =
- F.p_equal (F.e_get m1 ptr) (F.e_get m0 ptr) in
- let equal_assigned =
- F.p_equal (F.e_get m1 ptr) (F.e_get m_undef ptr) in
- let process = Tactical.insert ~at:s.id
- [ "Havoc",F.p_if separated equal_unassigned equal_assigned ] in
- Applicable process
- else
- ( feedback#set_error "Not a pointer type" ;
- Not_configured )
- else Not_configured
- | _ -> Not_applicable
- end
- | _ -> Not_applicable
+ method select _feedback sel =
+ let at = Tactical.at sel in
+ let e = Tactical.selected sel in
+ match lookup_havoc e with
+ | None -> Not_applicable
+ | Some(mr,m0,a,n,p) ->
+ let separated =
+ F.p_call MemTyped.p_separated
+ [ p ; F.e_int 1 ; a ; n ] in
+ let process = Tactical.rewrite ?at [
+ "Unassigned" , separated , e , F.e_get m0 p ;
+ "Assigned" , F.p_not separated , e , F.e_get mr p ;
+ ] in
+ Applicable process
end
(* -------------------------------------------------------------------------- *)
@@ -219,14 +195,13 @@ class validity =
module Havoc =
struct
- let field = field
let tactical = Tactical.export (new havoc)
- let strategy ?(priority=1.0) ~havoc ~addr =
+ let strategy ?(priority=1.0) ~havoc =
Strategy.{
priority ;
tactical ;
selection = havoc ;
- arguments = [ arg field addr ] ;
+ arguments = [] ;
}
end
diff --git a/src/plugins/wp/TacHavoc.mli b/src/plugins/wp/TacHavoc.mli
index 2ed3b403e084164a16fa9ea0f55a31c736348048..4d25edb8d32541f47afe6bd960e9538d640e7cc5 100644
--- a/src/plugins/wp/TacHavoc.mli
+++ b/src/plugins/wp/TacHavoc.mli
@@ -27,10 +27,9 @@ open Strategy
module Havoc :
sig
- val field : selection field
val tactical : tactical
val strategy :
- ?priority:float -> havoc:selection -> addr:selection -> strategy
+ ?priority:float -> havoc:selection -> strategy
end
module Separated :
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index ea227ab18ef8b10f42a02a49126f5baadf28f2cd..42eb158d5697eca2e09a93203747c05981c8d863 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -53,7 +53,6 @@ type bindings = (F.var * selection) list
type env = {
binder : L.binder ;
feedback : Tactical.feedback ;
- pool : Lang.F.pool ;
mutable index : int ;
}
@@ -154,7 +153,7 @@ class instance =
bindings, F.e_imply hs property
| L.Bind(q,tau,phi) , fd :: fields when q = env.binder ->
env.index <- succ env.index ;
- let x = F.fresh env.pool tau in
+ let x = F.fresh env.feedback#pool tau in
let v = self#get_field fd in
let range = match tau with L.Int -> true | _ -> false in
let tooltip = fieldname ~range env.index x in
@@ -171,9 +170,7 @@ class instance =
let binder = match side with None -> L.Exists | Some _ -> L.Forall in
let lemma = F.e_prop p in
if has_binder binder lemma then
- let vars = F.vars lemma in
- let pool = Lang.new_pool ~vars () in
- let env = { index = 0 ; feedback ; binder ; pool } in
+ let env = { index = 0 ; feedback ; binder } in
let bindings,phi = self#wrap env lemma fields in
if List.exists (fun (_,v) -> not (Tactical.is_empty v)) bindings
then
diff --git a/src/plugins/wp/TacSplit.ml b/src/plugins/wp/TacSplit.ml
index 88f3a2ba4ea3185fb46ef4a3e3ef311d597566cb..ac7a8919053453092eab3ece478e1c4a66edc8e4 100644
--- a/src/plugins/wp/TacSplit.ml
+++ b/src/plugins/wp/TacSplit.ml
@@ -24,7 +24,7 @@ open Lang
module PartitionsQQ : sig
val destructs_qq :
- Lang.F.pred ->
+ Lang.F.pool ->
Qed.Logic.binder -> tau:Lang.F.QED.tau -> phi:Lang.F.QED.bind ->
Lang.F.Vars.t * Lang.F.QED.term
@@ -35,12 +35,7 @@ end
let dkey = Wp_parameters.register_category "tac_split_quantifiers" (* debugging key *)
let debug fmt = Wp_parameters.debug ~dkey fmt
- let destructs_qq p qq ~tau ~phi =
- let pool =
- let quant = F.e_prop p in
- let vars = Lang.F.vars quant in
- Lang.new_pool ~vars ()
- in
+ let destructs_qq pool qq ~tau ~phi =
let rec destructs_qq vars ~tau ~phi =
let open Qed.Logic in
let x = F.fresh pool tau in
@@ -217,7 +212,7 @@ class split =
let open Qed.Logic in
match Lang.F.e_expr p with
| Bind (Exists,tau,phi) -> begin
- let vars,q = PartitionsQQ.destructs_qq p Exists ~tau ~phi in
+ let vars,q = PartitionsQQ.destructs_qq feedback#pool Exists ~tau ~phi in
match Lang.F.repr q with
| If (c,p,q) ->
if F.Vars.is_empty (F.Vars.inter (F.vars c) vars) then
@@ -326,7 +321,7 @@ class split =
let open Qed.Logic in
match F.e_expr p with
| Bind (Forall,tau,phi) -> begin
- let vars,q = PartitionsQQ.destructs_qq p Forall ~tau ~phi in
+ let vars,q = PartitionsQQ.destructs_qq feedback#pool Forall ~tau ~phi in
match Lang.F.repr q with
| If (c,p,q) ->
if F.Vars.is_empty (F.Vars.inter (F.vars c) vars) then
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index d49794b6cb54b829f016cc0e45db5cb5c43fc9d8..489b729091213327c6d50406a9c62ef78d40340e 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -316,6 +316,7 @@ type 'a formatter = ('a,Format.formatter,unit) format -> 'a
class type feedback =
object
+ method pool : pool
method interactive : bool
method get_title : string
method has_error : bool
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index f501602f64a148c810dcb1e447c33a779389a02c..c135567fe9fe67191b949604a845248dc0b9f962 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -142,6 +142,9 @@ type 'a formatter = ('a,Format.formatter,unit) format -> 'a
class type feedback =
object
+ (** Global fresh variable pool *)
+ method pool : pool
+
(** Interactive mode.
If [false] the GUI is not activated.
Hence, detailed feedback is not reported to the user. *)