Update installation instructions

- Refer to the existing opam package
- Indicates optional dependencies for deduction

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