diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml index 5aec0a471c1c9dd3b23dd1429d60ae609cc5c969..83ed15378f0441e321f85ab79717fc656015226e 100644 --- a/src/plugins/qed/logic.ml +++ b/src/plugins/qed/logic.ml @@ -308,7 +308,7 @@ sig val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> term -> (binder * var) list * term - (** Open all the specified binders (flags default to `true`, so all + (** Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default). The pool must contain all free variables of the term. *) diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli index 8e8e89519490e4f0d462cbd55ba14d38b8fc5119..d02b68cdb98e5ad7a59352b3c7e30d1680f45490 100644 --- a/src/plugins/wp/Lang.mli +++ b/src/plugins/wp/Lang.mli @@ -295,7 +295,7 @@ sig val e_open : pool:pool -> ?forall:bool -> ?exists:bool -> ?lambda:bool -> term -> (binder * var) list * term - (** Open all the specified binders (flags default to `true`, so all + (** Open all the specified binders (flags default to `true`, so all consecutive top most binders are opened by default). The pool must contain all free variables of the term. *)