From 1ed5f84b221bf52c935cd4441f5e050bdea3d09e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 25 Jun 2019 11:10:15 +0200
Subject: [PATCH] [qed] possible extensions of e-subst with let-intro
---
src/plugins/qed/term.ml | 7 +++++++
1 file changed, 7 insertions(+)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index df4a10e3c34..a1798c37812 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2166,10 +2166,17 @@ struct
let qs = (q,x) :: qs in
bind sigma alpha qs a
| _ ->
+ (* HERE:
+ This final binding of variables could be parallelized
+ if Bvars is precise enough *)
List.fold_left
(fun e (q,x) ->
if Vars.mem x e.vars then
let t = tau_of_var x in
+ (* HERE:
+ 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)
else e
) (subst sigma alpha e) qs
--
GitLab