remove errors in the documentation

1 files changed, 4 insertions, 3 deletions

diff --git a/README.md b/README.md
index 715019c268..86eeef5fd2 100644
--- a/README.md
+++ b/README.md
@@ -8,16 +8,17 @@ How to write plugins in Coq
     - To use it:
 
     `cd tuto0; make`
-    `coqtop -I src`
+    `coqtop -I src -R theories Tuto0`
 
-    In the Coq section type:  `Require ML Module "tuto0_plugin". HelloWorld.`
+    In the Coq session type:  `Require Tuto0.Loader. HelloWorld.`
 
   # tuto1 : Ocaml to Coq communication
   * Explore the memory of Coq, modify it
     - Commands that take arguments: strings, symbols, expressions of the calculus of constructions
     - Commands that interact with type-checking in Coq
     - A command that adds a new definition or theorem
-    - A command that uses a name and exploits the existing definitions or theorems
+    - A command that uses a name and exploits the existing definitions
+      or theorems
     - A command that exploits an existing ongoing proof
     - A commandthat defines a new tactic