From 9530cb4e9c2a6be19acef05f199c9b27db59b510 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Tue, 30 Jul 2019 11:03:39 +0200
Subject: [PATCH] [WP] Add to Lang.For_export rewriting for eq and leq
---
src/plugins/wp/Lang.ml | 4 ++++
src/plugins/wp/Lang.mli | 3 +++
2 files changed, 7 insertions(+)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2ba8603148d..b5b2010ef36 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 af9ac3bb08b..f4eb792d320 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
--
GitLab