diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index bfe4d75df24c91bf60afe227a14a1cdfc1dc59f3..2fb65326e84fd03ef57d016384cad71606deccec 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -39,8 +39,6 @@ open Sigs
 let cluster () =
   Definitions.cluster ~id:"Compound" ~title:"Memory Compound Loader" ()
 
-type frame = string * Definitions.trigger list * pred list * term * term
-
 module type Model =
 sig
 
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 6f94c256955700557f6736215d5e40c72eacb6ae..ddc2677cbc01eff8c56b345c59582ab40f103109 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -32,16 +32,6 @@ open Sigs
 
 val cluster : unit -> cluster
 
-(** Frame Conditions.
-    Consider a function [phi(m)] over memory [m],
-    we want memories [m1,m2] and condition [p] such that
-    [p(m1,m2) -> phi(m1) = phi(m2)].
-    - [name] used for generating lemma
-    - [triggers] for the lemma
-    - [conditions] for the frame lemma to hold
-    - [mem1,mem2] to two memories for which the lemma holds *)
-type frame = string * Definitions.trigger list * pred list * term * term
-
 (** Loader Model for Atomic Values *)
 module type Model =
 sig
diff --git a/src/plugins/wp/Sigs.ml b/src/plugins/wp/Sigs.ml
index 6fc72a241aaea9e0a3f4c1e465d17c476d787977..a91e7770466e5c1a0f78d4e638690af8a1c871c2 100644
--- a/src/plugins/wp/Sigs.ml
+++ b/src/plugins/wp/Sigs.ml
@@ -85,6 +85,16 @@ type 'a result =
 (** Polarity of predicate compilation *)
 type polarity = [ `Positive | `Negative | `NoPolarity ]
 
+(** Frame Conditions.
+    Consider a function [phi(m)] over memory [m],
+    we want memories [m1,m2] and condition [p] such that
+    [p(m1,m2) -> phi(m1) = phi(m2)].
+    - [name] used for generating lemma
+    - [triggers] for the lemma
+    - [conditions] for the frame lemma to hold
+    - [mem1,mem2] to two memories for which the lemma holds *)
+type frame = string * Definitions.trigger list * pred list * term * term
+
 (* -------------------------------------------------------------------------- *)
 (** {1 Reversing Models}