corrects a problem in documenting how to run the demo

1 files changed, 24 insertions, 15 deletions

diff --git a/README.md b/README.md
index 94a0b9da34..406bb1083c 100644
--- a/README.md
+++ b/README.md
@@ -14,30 +14,39 @@ How to write plugins in Coq
 
   In the Coq session type:
 ```coq
-    Require Tuto0.Loader. HelloWorld.
+    Require Import 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 exploits an existing ongoing proof
-    - A command that defines a new tactic
+  - 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 exploits an existing ongoing proof
+  - A command that defines a new tactic
 
+  Compilation and loading must be performed as for `tuto0`.
+  
   # tuto2 : Ocaml to Coq communication
   A more step by step introduction to writing commands
-    - Explanation of the syntax of entries
-    - Adding a new type to and parsing to the available choices
-    - Handling commands that store information in user-chosen registers and tables
+  - Explanation of the syntax of entries
+  - Adding a new type to and parsing to the available choices
+  - Handling commands that store information in user-chosen registers and tables
 
+  Compilation and loading must be performed as for `tuto1`.
 
   # tuto3 : manipulating terms of the calculus of constructions
-  obtaining existing values from memory and composing them, making sure
-  they are well-typed, and using them in new definitions and proofs.
-    - 
-  
+  Manipulating terms, inside commands and tactics.
+  - Obtaining existing values from memory
+  - Composing values
+  - Verifying types
+  - Leveraging type inference
+  - Leveraging coercion
+  - Using these terms in commands
+  - Using these terms in tactics
+
+  compilation and loading must be performed as for `tuto0`.
     
     
\ No newline at end of file