diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7247b98f777a66311e4bfd3e38dbe9dc26262e0c..1e67b356c3f30cb659e8badb3f4247bfcb2326aa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,4 +1,8 @@
-# Current development
+# Version 0.3
+
+- compatibility with Frama-C 25.0 Manganese
+
+# Version 0.2
 
 - add warning category `unknown-func` which aborts by default
 - add `\func` meta-variables in all contexts
diff --git a/README.md b/README.md
index fd895ae58b56d2505a5aa86ff24e8a822fba43e5..cd3fa9517390f801c43d528d0e98565c37471709 100644
--- a/README.md
+++ b/README.md
@@ -7,8 +7,17 @@ constraints easily.  For more information, see [[2]](#paper).
 
 ## Installation
 
-If your Frama-C is installed via `opam`, you just have to run `opam install .`  
-Otherwise, run the usual `autoconf && ./configure && make && make install`
+You can install a stable version of MetAcsl through [`opam`](https://opam.ocaml.org) (package `frama-c-metacsl`).
+
+If you want to compile it manually from the git repository, you need to have Frama-C installed,
+and to ensure that the MetAcsl branch you intend to work on is compatible with it
+(NB: the `master` branches from both repositories are supposed to stay synchronized).
+
+Optional dependencies, needed for using the [deduction](#deduction) capabilities of MetAcsl include:
+- [Why3](https://why3.lri.fr) (only for checking the consistency of MetAcsl's deduction model)
+- [SWI Prolog](https://www.swi-prolog.org/)
+
+Then, run the usual `autoconf && ./configure && make && make install`
 
 ## Usage
 
@@ -333,7 +342,7 @@ particular may pose problem. If a limit on the size of the set can be
 determined, on can use `-meta-static-bindings L` to use static arrays of size L
 instead.
 
-### Deduction (experimental) 
+### Deduction (experimental) <a name="deduction"></a>
 
 In some specific cases, MetAcsl is able to deduce a meta-property from others.
 Such a deduction must be manually requested by the `proof:deduce` flag. For the
diff --git a/frama-c-metacsl.opam b/frama-c-metacsl.opam
index 12bcb503d8f2b7a5de051b2b9af2c871e2f3bcd3..0b424436c407887251470127dd29b6ffc5c242b2 100644
--- a/frama-c-metacsl.opam
+++ b/frama-c-metacsl.opam
@@ -36,7 +36,7 @@ build: [
 ]
 name: "frama-c-metacsl"
 synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.2"
+version: "0.3+dev"
 description:"""
 MetACSL let users write properties that need to be checked at particular
 contexts (e.g. each time a location is written to inside a given set
diff --git a/frama-c-metacsl.opam.template b/frama-c-metacsl.opam.template
index 5a347d28739771109acd2d47307b7bbd5acd5cb1..b74abebeffdf9b5c35152c2636475e751436571f 100644
--- a/frama-c-metacsl.opam.template
+++ b/frama-c-metacsl.opam.template
@@ -1,6 +1,6 @@
 name: "frama-c-metacsl"
 synopsis: "MetACSL plugin of Frama-C for writing pervasives properties"
-version: "0.2"
+version: "0.3+dev"
 description:"""
 MetACSL let users write properties that need to be checked at particular
 contexts (e.g. each time a location is written to inside a given set