From 445a43f38253bf1b3288f38073da14a869f9e0f5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 22 Oct 2019 14:40:38 +0200
Subject: [PATCH] [wp] fix unecessary int-power

---
 src/plugins/wp/share/ergo/real.PowerReal.mlw | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/src/plugins/wp/share/ergo/real.PowerReal.mlw b/src/plugins/wp/share/ergo/real.PowerReal.mlw
index 97f8c3d547e..140f336820e 100644
--- a/src/plugins/wp/share/ergo/real.PowerReal.mlw
+++ b/src/plugins/wp/share/ergo/real.PowerReal.mlw
@@ -48,8 +48,3 @@ axiom Pow_one_y : (forall y:real. (pow(1.0, y) = 1.0))
 axiom Pow_x_two : (forall x:real. ((0.0 <  x) -> (pow(x, 2.0) = sqr(x))))
 
 axiom Pow_half : (forall x:real. ((0.0 <  x) -> (pow(x, 0.5) = sqrt(x))))
-
-axiom pow_from_int :
-  (forall x:int. forall y:int. ((0 <  x) -> ((0 <= y) -> (pow(from_int(x),
-  from_int(y)) = from_int(power(x, y))))))
-
-- 
GitLab