diff --git a/Makefile.in b/Makefile.in
index 5ba680be014950165ef7c9098023338fbb23f720..5d170258974a593497dcef46325a605b9a70c7b5 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -837,7 +837,7 @@ ifeq (@enable_coq_libs@,yes)
 COQLIBS_INT_FILES = Abs ComputerDivision EuclideanDivision Int MinMax
 COQLIBS_INT = $(addprefix lib/coq/int/, $(COQLIBS_INT_FILES))
 
-COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square
+COQLIBS_REAL_FILES = Abs ExpLog FromInt MinMax Real Square RealInfix
 COQLIBS_REAL = $(addprefix lib/coq/real/, $(COQLIBS_REAL_FILES))
 
 ifeq (@enable_coq_fp_libs@,yes)
diff --git a/ROADMAP b/ROADMAP
index cf717de742d923bf66eb87a328f782ad7c24d411..f9cd789787fd86cdd5e855e1447c934d3f8b9983 100644
--- a/ROADMAP
+++ b/ROADMAP
@@ -133,8 +133,12 @@ https://gforge.inria.fr/tracker/index.php?func=detail&aid=13736&group_id=2990
    ne pas oublier de dire que les dependances avec le .why ou .mlw: ne sera pas vérifié
  - (WHO?) revoir documentation du smoke detector
  - (WHO?) Documenter l'utilisation de plusieurs version du meme prouveur comme CVC3 et Z3
- - (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé
-   ET LES METTRE AU POINT
+ - (CLAUDE) Documenter les popups qui peuvent apparaitre dans why3ide quand les prouveurs ont changé. Et les mettre au point:
+   . Lors d'un replay, le dialogue "replace proof" apparait un nombre important de fois,
+     il faut absolument pouvoir interrompre, ou donner une reponse qui soit appliquée pour le reste.
+     (le 3e bouton "never replace..." ne semble pas jourer ce role...)
+   . le dialogue "replace proof" est de toute facon trop large, et les choix possibles sont confus.
+
  - DONE (ANDREI) ajouter option a why3config pour ajouter association ident-executable
  - (CLAUDE) meme ordre d'idee: ne pas ecraser "default editor" et "timelimit"
  - (WHO?) complete api.tex: explain how to build theories, apply
diff --git a/drivers/coq-common.gen b/drivers/coq-common.gen
index dd4f06540c8e9fec6d60f2a3ce0e9da18a8aa12f..454aa8147830505484e1055b6f186381ea591d30 100644
--- a/drivers/coq-common.gen
+++ b/drivers/coq-common.gen
@@ -256,11 +256,20 @@ theory real.ExpLog
 end
 
 
-theory real.Power
+theory real.PowerInt
 
   prelude "Require Import Rpower."
 
-  (* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *)
+  syntax function power "(powerRZ %1)"
+
+end
+
+theory real.PowerReal
+
+  prelude "Require Import Rpower."
+
+  syntax function pow "(Rpower %1)"
+
 end
 
 theory real.Trigonometry
diff --git a/drivers/pvs-common.gen b/drivers/pvs-common.gen
index 891cb602ceccb45e6ec21262b6d432819eb9827c..2fd2958ae7e128b545952f7b2a3bf0d08c3217c8 100644
--- a/drivers/pvs-common.gen
+++ b/drivers/pvs-common.gen
@@ -242,7 +242,7 @@ theory real.ExpLog
 
 end
 
-theory real.Power
+theory real.PowerReal
 
   syntax function pow "(%1 ^ %2)"
 
diff --git a/examples/check-builtin/real.why b/examples/check-builtin/real.why
index ded841c2315053b455d5b4d612a11bed155a0496..434a5109c62c97a9d52b64689dde4d38ea07d2ab 100644
--- a/examples/check-builtin/real.why
+++ b/examples/check-builtin/real.why
@@ -2,5 +2,15 @@ theory Test
   use import real.Real
   goal G1 : 5.5 * 10. = 55.
   goal G2 : 9. / 3. = 3.
-  goal G3 : inv(5.) = 0.2
+  goal G3 : inv 5. = 0.2
+end
+
+theory TestInfix
+  use import real.RealInfix
+  goal Add : 5.5 +. 10. = 15.5
+  goal Sub : 9. -. 3. = 6.
+  goal Neg : -. 5. +. 3.5 = -. 1.5
+  goal Mul : 5.5 *. 10. = 55.
+  goal Div : 9. /. 2. = 4.5
+  goal Inv : inv 5. = 0.2
 end
diff --git a/examples/check-builtin/real/why3session.xml b/examples/check-builtin/real/why3session.xml
index b4063c81c3c4fba124a23ecfa10b586ed9770c13..54e1cd10ba172e53214fcf94f6e4ed41aad39491 100644
--- a/examples/check-builtin/real/why3session.xml
+++ b/examples/check-builtin/real/why3session.xml
@@ -1,7 +1,7 @@
 <?xml version="1.0" encoding="UTF-8"?>
 <!DOCTYPE why3session SYSTEM "why3session.dtd">
 <why3session
- name="check-builtin/real/why3session.xml">
+ name="real/why3session.xml">
  <prover
   id="0"
   name="Alt-Ergo"
@@ -12,64 +12,86 @@
   version="2.2"/>
  <prover
   id="2"
-  name="Spass"
-  version="3.7"/>
+  name="CVC3"
+  version="2.4.1"/>
  <prover
   id="3"
+  name="Gappa"
+  version="0.16.0"/>
+ <prover
+  id="4"
   name="Yices"
   version="1.0.25"/>
  <prover
-  id="4"
+  id="5"
   name="Z3"
   version="2.19"/>
+ <prover
+  id="6"
+  name="Z3"
+  version="3.2"/>
  <file
   name="../real.why"
   verified="true"
-  expanded="false">
+  expanded="true">
   <theory
    name="Test"
-   locfile="check-builtin/real/../real.why"
+   locfile="real/../real.why"
    loclnum="1" loccnumb="7" loccnume="11"
    verified="true"
    expanded="true">
    <goal
     name="G1"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="3" loccnumb="7" loccnume="9"
     sum="7961c96b42f34e5cb3280ce85643dffb"
     proved="true"
     expanded="true"
     shape="ainfix =ainfix *c5.5c10.c55.">
     <proof
-     prover="4"
-     timelimit="10"
+     prover="5"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="2"
-     timelimit="10"
+     prover="1"
+     timelimit="3"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.20"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="1"
-     timelimit="10"
+     prover="0"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="0"
-     timelimit="10"
+     prover="2"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="4"
      timelimit="10"
      obsolete="false"
      archived="false">
@@ -78,36 +100,50 @@
    </goal>
    <goal
     name="G2"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="4" loccnumb="7" loccnume="9"
     sum="b18a4b0fb8e663468863ba1c86a7cc64"
     proved="true"
     expanded="true"
     shape="ainfix =ainfix /c9.c3.c3.">
     <proof
-     prover="4"
-     timelimit="10"
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="2"
-     timelimit="10"
+     timelimit="3"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.47"/>
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="1"
-     timelimit="10"
+     prover="3"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
-     prover="0"
-     timelimit="10"
+     prover="6"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
@@ -115,36 +151,363 @@
    </goal>
    <goal
     name="G3"
-    locfile="check-builtin/real/../real.why"
+    locfile="real/../real.why"
     loclnum="5" loccnumb="7" loccnume="9"
     sum="297dff92907d47bda80a8ffe2d186396"
     proved="true"
     expanded="true"
     shape="ainfix =ainvc5.c0.2">
     <proof
-     prover="4"
-     timelimit="10"
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="2"
-     timelimit="10"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="10.08"/>
+     <result status="failure" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+  </theory>
+  <theory
+   name="TestInfix"
+   locfile="real/../real.why"
+   loclnum="8" loccnumb="7" loccnume="16"
+   verified="true"
+   expanded="true">
+   <goal
+    name="Add"
+    locfile="real/../real.why"
+    loclnum="10" loccnumb="7" loccnume="10"
+    sum="43afbf3638f15444ec33376879694c6b"
+    proved="true"
+    expanded="true"
+    shape="ainfix =ainfix +.c5.5c10.c15.5">
+    <proof
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="1"
-     timelimit="10"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
     </proof>
     <proof
      prover="0"
-     timelimit="10"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Sub"
+    locfile="real/../real.why"
+    loclnum="11" loccnumb="7" loccnume="10"
+    sum="9e26dca43231665f3c20276262e0e4ef"
+    proved="true"
+    expanded="true"
+    shape="ainfix =ainfix -.c9.c3.c6.">
+    <proof
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Neg"
+    locfile="real/../real.why"
+    loclnum="12" loccnumb="7" loccnume="10"
+    sum="4f3a94d0b96c33ec0276c6802921cd6a"
+    proved="true"
+    expanded="true"
+    shape="ainfix =ainfix +.aprefix -.c5.c3.5aprefix -.c1.5">
+    <proof
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Mul"
+    locfile="real/../real.why"
+    loclnum="13" loccnumb="7" loccnume="10"
+    sum="547a086bd1da4bd6a329f80d539f9e4f"
+    proved="true"
+    expanded="true"
+    shape="ainfix =ainfix *.c5.5c10.c55.">
+    <proof
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Div"
+    locfile="real/../real.why"
+    loclnum="14" loccnumb="7" loccnume="10"
+    sum="11f3cf0fd8346c98624030a58cf9940a"
+    proved="true"
+    expanded="true"
+    shape="ainfix =ainfix /.c9.c2.c4.5">
+    <proof
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+   </goal>
+   <goal
+    name="Inv"
+    locfile="real/../real.why"
+    loclnum="15" loccnumb="7" loccnume="10"
+    sum="70900cabfcc887614c28215d0ac16b18"
+    proved="true"
+    expanded="true"
+    shape="ainfix =ainvc5.c0.2">
+    <proof
+     prover="5"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="1"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="0"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="2"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="valid" time="0.00"/>
+    </proof>
+    <proof
+     prover="3"
+     timelimit="3"
+     obsolete="false"
+     archived="false">
+     <result status="failure" time="0.00"/>
+    </proof>
+    <proof
+     prover="6"
+     timelimit="3"
      obsolete="false"
      archived="false">
      <result status="valid" time="0.00"/>
diff --git a/lib/coq/real/RealInfix.v b/lib/coq/real/RealInfix.v
new file mode 100644
index 0000000000000000000000000000000000000000..cb3404443a61fecb238b9f460d4501d6b5d8b78d
--- /dev/null
+++ b/lib/coq/real/RealInfix.v
@@ -0,0 +1,7 @@
+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import ZArith.
+Require Import Rbase.
+Require real.Real.
+
+
diff --git a/theories/real.why b/theories/real.why
index 0e0269e0628313213c0996e9a46ce61717d03833..b4c424d29b78a61d6f601de874dbd7c917060d44 100644
--- a/theories/real.why
+++ b/theories/real.why
@@ -26,6 +26,7 @@ theory RealInfix
   function ( *.) (x:real) (y:real) : real = x * y
   function (/.) (x:real) (y:real) : real = x / y
   function (-._) (x:real) : real = - x
+  function inv (x:real) : real = Real.inv x
 
   predicate (<=.) (x:real) (y:real) = x <= y
   predicate (>=.) (x:real) (y:real) = x >= y
@@ -220,7 +221,27 @@ theory ExpLogTest
 end
 
 
-theory Power
+theory PowerInt
+
+  use int.Int
+  use Real
+
+  clone export int.Exponentiation with
+    type t = real, constant one = Real.one, function (*) = Real.(*)
+
+
+end
+
+theory PowerIntTest
+
+  use import PowerInt
+
+  lemma Pow_2_2 : power 2.0 2 = 4.0
+
+end
+
+
+theory PowerReal
 
   use import Real
   use import Square
@@ -251,9 +272,9 @@ theory Power
 
 end
 
-theory PowerTest
+theory PowerRealTest
 
-  use import Power
+  use import PowerReal
 
   lemma Pow_2_2 : pow 2.0 2.0 = 4.0