Project clean with appropriate README

README.md

@@ -18,12 +18,15 @@ autopilots.
 * [Menhir](http://gitlab.inria.fr/fpottier/menhir) (tested with version 20220210)
 * [Coq-Mathcomp-SSReflect](https://math-comp.github.io) (tested with version 1.15.0)
 
-The dependencies can be installed using [OPAM](https://opam.ocaml.org)
-(version 2.0 or later):
+The dependencies are already installed using [OPAM](https://opam.ocaml.org)
+(version 2.0 or later).
+
+Before doing anything, make sure that you are in the switch opam local that has
+been created to avoid being in conflict with the opam environment by default
+that Paparazzi uses.
 
 ```bash
-opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq ocamlbuild xml-light menhir coq-mathcomp-ssreflect coq-menhirlib 
+eval $(opam env)
 ```
 
 To generate the documentation, the package `graphviz` must be installed:
@@ -35,7 +38,6 @@ sudo apt install graphviz
 ## Using the Generator
 
 The project needs the source of
-[Paparazzi](https://github.com/paparazzi/paparazzi) and
 [CompCert](https://github.com/AbsInt/CompCert)@8d21a7fa. The sources must
 be modified and compiled in order to use the generator. These steps can be
 easily retrieved with the following script.
@@ -44,7 +46,11 @@ easily retrieved with the following script.
 ./configure
 ```
 
-The generator can then be built using the Makefile.
+The project doesn't need anymore the source of
+[Paparazzi](https://github.com/paparazzi/paparazzi), modifications have been
+done to directly use Paparazzi which is situated above in the tree structure.
+
+The generator can then be built using the Makefile. 
 
 ```bash
 make build
@@ -52,20 +58,27 @@ make build
 
 The description of the build process is described [here](./docs/build.md)
 
-The generator can then be used with the following command:
+The Makefile can also launch tests to make sure everything works.
 
 ```bash
-export PAPARAZZI_HOME=`pwd`/paparazzi
-./vfpg.native [XML input file] [C output file]
+make tests
 ```
 
-The Makefile can also launch tests.
+All the tests available are described [here](./docs/tests.md)
+
+The generator can then be used into the Paparazzi Center with the following
+commands :
 
 ```bash
-make tests
+cd ../../..
+eval $(opam env)
+make
+./paparazzi
 ```
 
-All the tests available are described [here](./docs/tests.md)
+Make sure you do those commands in a terminal and not in vscode for example.
+From now on you can choose between the old generator, named "Ocaml" or the new
+generator which is VFPG, named "Verified with Coq".
 
 ## Description of folders in the project