From 61bf9d47bbcfde7123f800311c6cb6817e37ff38 Mon Sep 17 00:00:00 2001
From: Yves Bertot
Date: Fri, 4 May 2018 17:43:28 +0200
Subject: remove errors in the documentation

---
 README.md | 7 ++++---
 1 file 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
 
-- 
cgit v1.2.3