diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2ba8603148d81bef9b2ec9b53360ab91c4c5bf55..b5b2010ef36b168df4281e1a6034a921e207da51 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -1001,6 +1001,10 @@ module For_export = struct
     add_init (fun () -> QZERO.set_builtin f c)
   let set_builtin' f c =
     add_init (fun () -> QZERO.set_builtin' f c)
+  let set_builtin_eq f c =
+    add_init (fun () -> QZERO.set_builtin_eq f c)
+  let set_builtin_leq f c =
+    add_init (fun () -> QZERO.set_builtin_leq f c)
 
   let in_state f v = QZERO.in_state (get_state ()) f v
 
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index af9ac3bb08b228a2aed5effed33e13389dfdddff..f4eb792d3209e0adb160e7de564dd092fd698625 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -604,6 +604,9 @@ module For_export : sig
   val set_builtin : Fun.t -> (term list -> term) -> unit
   val set_builtin' : Fun.t -> (term list -> tau option -> term) -> unit
 
+  val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
+  val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
+
   val in_state: ('a -> 'b) -> 'a -> 'b
 
 end