From 944bb98c44228a5edd56db410caf63ad58d91850 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 4 Feb 2019 10:10:30 +0100
Subject: [PATCH] [Qed] optimise lc-open
---
src/plugins/qed/term.ml | 7 ++++---
1 file changed, 4 insertions(+), 3 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 99e54cad0af..0c05374f3a1 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
--
GitLab