From a84ae7af146d469c95aabc000a8753c89936ff0e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 28 Jun 2019 12:46:52 +0200
Subject: [PATCH] [wp] activate defensive agains for subst
---
src/plugins/qed/term.ml | 6 ++++--
1 file changed, 4 insertions(+), 2 deletions(-)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 430d87177b9..2ab6b9b4d99 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2080,7 +2080,7 @@ struct
}
let validate fn e =
- if false && not (lc_closed e) then
+ if not (lc_closed e) then
begin
Format.eprintf "Invalid %s: %a@." fn pretty e ;
raise (Invalid_argument (fn ^ ": non lc-closed binding"))
@@ -2167,7 +2167,9 @@ struct
apply sigma Intmap.empty (phi e) (List.map phi es)
| _ -> rebuild (incache mu sigma alpha) e
in
- (if lc_closed e && lc_closed r then Subst.add sigma e r) ; r
+ (* Only put closed terms in cache *)
+ (if lc_closed e && lc_closed r then Subst.add sigma e r) ;
+ (* Finally returns result *) r
and bind sigma alpha qs e =
match e.repr with
--
GitLab