diff --git a/ROADMAP b/ROADMAP
index 0485f37501a9307d76f9b37b07c62e9d385dfa9c..c2b0485417270958c95253b6e77dc81787c17a94 100644
--- a/ROADMAP
+++ b/ROADMAP
@@ -89,11 +89,11 @@
 ** The last commit:
 *** increment the magic number in config
 *** add a tag to the git repository
-*** The next commit : increment de why3 version
+*** The next commit : increment why3 version
 
-* YET TO DO
-** fix bug with term shapes, not taking triggers into account
-** remove prover coq-relize
+* misc
+** DONE fix bug with term shapes, not taking triggers into account
+** DONE remove prover coq-realize
 
 * prover support
 ** DONE test/debug TPTP output, make Vampire work
diff --git a/examples/hoare_logic/imp/why3session.xml b/examples/hoare_logic/imp/why3session.xml
index d6cba97535162e36291af38e01a902be7ee61c05..34e9b0ef485a6599a758d888e30ee6935477d1d0 100644
--- a/examples/hoare_logic/imp/why3session.xml
+++ b/examples/hoare_logic/imp/why3session.xml
@@ -10,10 +10,6 @@
   id="coq"
   name="Coq"
   version="8.2pl1"/>
- <prover
-  id="coq-realize"
-  name="Coq Realize"
-  version="8.2pl1"/>
  <prover
   id="cvc3"
   name="CVC3"
diff --git a/share/provers-detection-data.conf.in b/share/provers-detection-data.conf.in
index 9f83bd46ad116019e7ba8afc5f8e855030347c46..1dcd5447b2dd17715a296e05f77acb5d3c8d0bd7 100644
--- a/share/provers-detection-data.conf.in
+++ b/share/provers-detection-data.conf.in
@@ -169,23 +169,6 @@ version_old = "1.3"
 command = "@LOCALBIN@why3-cpulimit %t %m -s %e -smt %f"
 driver = "drivers/z3_smtv1.drv"
 
-[ITP coq-realize]
-name = "Coq Realize"
-exec = "coqc"
-version_switch = "-v"
-version_regexp = "The Coq Proof Assistant, version \\([^ \n]+\\)"
-version_ok = "8.3pl2"
-version_ok = "8.3pl1"
-version_ok = "8.3"
-version_ok = "8.2pl2"
-version_ok = "8.2pl1"
-version_ok = "8.2"
-version_old = "8.1"
-version_old = "8.0"
-command = "@LOCALBIN@why3-cpulimit 0 %m -s %e %f"
-driver = "drivers/coq-realize.drv"
-editor = "coqide"
-
 [ITP coq]
 name = "Coq"
 exec = "coqc"