From e7b50a5d14a8451ffba779e832b82ea7c573903a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 25 Jun 2019 13:41:51 +0200
Subject: [PATCH] [qed] update docs
---
src/plugins/qed/logic.ml | 7 ++++---
src/plugins/qed/term.ml | 5 +----
2 files changed, 5 insertions(+), 7 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index f117f234c12..6620c41a9b3 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -306,9 +306,10 @@ sig
(** Bind the given variable if it appears free in the term,
or return the term unchanged. *)
- val e_open : ?pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
+ val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool ->
term -> (binder * var) list * term
- (** Open all the specified binders *)
+ (** Open all the specified binders
+ The pool must contain all free variables of the term. *)
val e_close : (binder * var) list -> term -> term
(** Closes all specified binders *)
@@ -348,7 +349,7 @@ sig
(** Must bind lc-closed terms, or raise Invalid_argument *)
val add_filter : t -> (term -> bool) -> unit
- (** Only modifies terms that {i not} pass the filter. *)
+ (** Only modifies terms that {i pass} the filter. *)
val add_var : t -> var -> unit
(** To the pool *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index b477ebcf576..58b7ee820bf 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2302,12 +2302,9 @@ struct
let e_exists = bind_xs Exists
let e_lambda = bind_xs Lambda
- let e_open ?pool ?(forall=true) ?(exists=true) ?(lambda=true) a =
+ let e_open ~pool ?(forall=true) ?(exists=true) ?(lambda=true) a =
match a.repr with
| Bind _ ->
- let pool = match pool with Some p -> p | None ->
- let p = POOL.create () in
- Vars.iter (POOL.add p) a.vars ; p in
let filter = function
| Forall -> forall
| Exists -> exists
--
GitLab