From 4759892d3168e31e784ef9367d93f4f80a202ca4 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 9 Oct 2020 16:15:35 +0200
Subject: [PATCH] [wp] protect functional sigma from unclosed terms
---
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 bc8331ad3c9..a2ce1c72e39 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2239,8 +2239,10 @@ struct
let fresh sigma t = fresh sigma.pool t
let call f e =
- let v = f e in
- validate "Qed.Subst.add_fun" v ; v
+ if lc_closed e then
+ let v = f e in
+ validate "Qed.Subst.add_fun" v ; v
+ else raise Not_found
let rec compute e = function
| EMPTY -> raise Not_found
--
GitLab