From a56ee38b60aba96de3f466c1536cfae6d115e94c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 18 Nov 2021 14:40:35 +0100
Subject: [PATCH] [wp] unused Ground.singleton
---
src/plugins/wp/Letify.ml | 6 ------
src/plugins/wp/Letify.mli | 3 ---
2 files changed, 9 deletions(-)
diff --git a/src/plugins/wp/Letify.ml b/src/plugins/wp/Letify.ml
index f975167c3ed..0e792d0961d 100644
--- a/src/plugins/wp/Letify.ml
+++ b/src/plugins/wp/Letify.ml
@@ -38,7 +38,6 @@ let occurs xs a = Vars.intersect xs (F.vars a)
module Ground =
struct
- type subst = pred -> pred
type env = {
mutable ground : bool Tmap.t ;
sigma : F.sigma ;
@@ -125,11 +124,6 @@ struct
let top () = { ground = Tmap.empty ; sigma = Lang.sigma () }
let copy env = { ground = env.ground ; sigma = Subst.copy env.sigma }
- let singleton p =
- let env = top () in
- ignore (assume env p) ;
- p_apply env
-
let branch env p =
let p = p_apply env p in
let wa = copy env in
diff --git a/src/plugins/wp/Letify.mli b/src/plugins/wp/Letify.mli
index 2f3d146ed9e..5e32818fe2e 100644
--- a/src/plugins/wp/Letify.mli
+++ b/src/plugins/wp/Letify.mli
@@ -29,9 +29,6 @@ open Lang.F
module Ground :
sig
- type subst = pred -> pred
- val singleton : pred -> subst
-
type env
val top : unit -> env
val copy : env -> env
--
GitLab