From 1a05d45a5000fd593f3844d39f14486d982bf085 Mon Sep 17 00:00:00 2001
From: ploc <ploc@garoche.net>
Date: Thu, 15 Nov 2018 22:19:43 -0800
Subject: [PATCH] Cleaning warning in mpfr

---
 src/plugins/mpfr/mpfr.ml | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/src/plugins/mpfr/mpfr.ml b/src/plugins/mpfr/mpfr.ml
index b6f1048d..3dacceeb 100644
--- a/src/plugins/mpfr/mpfr.ml
+++ b/src/plugins/mpfr/mpfr.ml
@@ -123,9 +123,6 @@ let base_inject_op id =
   | "sqrt" -> "MPFRsqrt"
   | "trunc" -> "MPFRtrunc"
   | "tan" -> "MPFRtan"
-
-           
-  | "pow"    -> "MPFRpow"
   | _        -> raise Not_found
 
 let inject_op id =
-- 
GitLab