From 03562e22f17d653c498848d97ec1f86de6991694 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 5 Jan 2022 13:37:55 +0100
Subject: [PATCH] [wp] Removes references to native:alt-ergo
---
opam/opam | 2 --
share/autocomplete_frama-c | 2 +-
2 files changed, 1 insertion(+), 3 deletions(-)
diff --git a/opam/opam b/opam/opam
index 8c4fd47361c..da3874d70e0 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 0637900a8bc..9c996616dc1 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" ]]
--
GitLab