From adf93e9ce4fb9285104ee24995eca2643f709190 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 27 Jun 2019 22:24:20 +0200
Subject: [PATCH] [wp] deprecates lc_open (for counter-examples)
---
src/plugins/qed/logic.ml | 3 +++
src/plugins/qed/term.ml | 6 +++---
2 files changed, 6 insertions(+), 3 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index fda9a5b9687..a451922eb1f 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -306,6 +306,9 @@ sig
(** Bind the given variable if it appears free in the term,
or return the term unchanged. *)
+ val lc_open : var -> lc_term -> term
+ [@@deprecated "Use e_unbind instead"]
+
val e_unbind : var -> lc_term -> term
(** Opens the top-most bound variable with a (fresh) variable.
Can be only applied on top-most lc-term from `Bind(_,_,_)`,
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index e6311444b09..1c3ca9819c3 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2004,7 +2004,7 @@ struct
| Bind(q,t,e) -> c_bind q t (f e)
(* Alpha-convert free-variable x with the top-most bound variable *)
- let lc_bind x (lc : lc_term) : lc_term =
+ let lc_close x (lc : lc_term) : lc_term =
let rec walk mu x lc =
if Vars.mem x lc.vars then
get mu (lc_alpha (walk mu x)) lc
@@ -2170,7 +2170,7 @@ struct
possible to insert a recursive call to let-intro
it will use a new instance of e_subst_var that
will work on a different sigma *)
- c_bind q t (lc_bind x e)
+ c_bind q t (lc_close x e)
else e
) (subst sigma alpha e) qs
@@ -2302,7 +2302,7 @@ struct
match q with Forall | Exists -> Vars.mem x e.vars | Lambda -> true in
if do_bind then
match let_intro_case q x e with
- | None -> c_bind q (tau_of_var x) (lc_bind x e)
+ | None -> c_bind q (tau_of_var x) (lc_close x e)
| Some v -> e_subst_var x v e (* case [let x = v ; e] *)
else e
--
GitLab