diff --git a/opam/opam b/opam/opam
index 8c4fd47361cd5bea9784716776d3495df456df11..da3874d70e0f39db1f87982bee7664efe60adad0 100644
--- a/opam/opam
+++ b/opam/opam
@@ -138,8 +138,6 @@ depopts: [
 ]
 
 messages: [
-  "The Frama-C/Wp now uses Why-3 for all provers (Cf. deprecated -wp-prover native:alt-ergo)"
-  {alt-ergo:installed}
   "The Frama-C/Wp native support for Coq is deprecated and only activated with Coq.8.13.x (use TIP or Why-3 instead)."
   {coq:installed}
 ]
diff --git a/share/autocomplete_frama-c b/share/autocomplete_frama-c
index 0637900a8bc57ac7f9d94af7d12540bbb93ca1b9..9c996616dc130fe18d77ed34128ef64b1c33565d 100644
--- a/share/autocomplete_frama-c
+++ b/share/autocomplete_frama-c
@@ -94,7 +94,7 @@ _frama-c ()
   then
       local prefix=; [[ $cur == *,* ]] && prefix="${cur%,*},"
       advance_options="$(frama-c -wp-detect | grep -E -o " \[.*" | grep -E -o "[^][|]*")"
-      advance_options+=" none script tip native:alt-ergo native:coq native:coqide"
+      advance_options+=" none script tip native:coq native:coqide"
       local ambigous="$(bind -v | grep show-all-if-ambiguous)"
       ambigous="${ambigous##* }"
       if [[ "$ambigous" == "on" ]]