diff --git a/src/plugins/qed/logic.mli b/src/plugins/qed/logic.mli
index 9fc9da009202ab67e73fd3bac4a3683a15728dd1..cf4f9df3ffe5908597b80e3f05e96424bd17041c 100644
--- a/src/plugins/qed/logic.mli
+++ b/src/plugins/qed/logic.mli
@@ -332,6 +332,7 @@ sig
   sig
     type t = sigma
     val create : ?pool:pool -> unit -> t
+    val copy : sigma -> sigma
 
     val fresh : t -> tau -> var
     val find : t -> term -> term
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 1809bf717026fbd1dbbea801eb19a086b9bfdc5f..aa7fc81b4b734aee1456958d25670fec6a1a03da 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2225,6 +2225,12 @@ struct
       filter = [] ;
     }
 
+    let copy sigma = {
+      pool = POOL.create ~copy:sigma.pool () ;
+      shared = sigma.shared ;
+      filter = sigma.filter ;
+    }
+
     let validate fn e =
       if not (lc_closed e) then
         begin
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index dc8cd859a31d70d4cbcc5f9c496e6891465173ed..4e10985cd28c99a2d565569613e52328b20fc71c 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -376,6 +376,7 @@ sig
 
   module Subst :
   sig
+    val copy : sigma -> sigma
     val find : sigma -> term -> term
     val add : sigma -> term -> term -> unit
     val add_map : sigma -> term Tmap.t -> unit