Clean, document, and expand plugin tutorials 0 and 1

1 files changed, 15 insertions, 23 deletions

diff --git a/doc/plugin_tutorial/README.md b/doc/plugin_tutorial/README.md
index f82edb2352..6d142a9af8 100644
--- a/doc/plugin_tutorial/README.md
+++ b/doc/plugin_tutorial/README.md
@@ -1,34 +1,20 @@
 How to write plugins in Coq
 ===========================
-  # Working environment : merlin, tuareg (open question)
+  # Working environment
+
+  In addition to installing OCaml and Coq, it can help to install several tools for development.
   
-  ## OCaml & related tools
+  ## Merlin
 
   These instructions use [OPAM](http://opam.ocaml.org/doc/Install.html)
 
 ```shell
-opam init --root=$PWD/CIW2018 --compiler=4.06.0 -j2
-eval `opam config env --root=$PWD/CIW2018`
-opam install camlp5 ocamlfind num # Coq's dependencies
-opam install lablgtk              # Coqide's dependencies (optional)
 opam install merlin               # prints instructions for vim and emacs
 ```
 
-  ## Coq
-
-```shell
-git clone git@github.com:coq/coq.git
-cd coq
-./configure -profile devel
-make -j2
-cd ..
-export PATH=$PWD/coq/bin:$PATH
-```
-
   ## This tutorial
 
 ```shell
-git clone git@github.com:ybertot/plugin_tutorials.git
 cd plugin_tutorials/tuto0
 make .merlin                # run before opening .ml files in your editor
 make                        # build
@@ -40,6 +26,8 @@ make                        # build
   package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject`
   - Example of syntax to add a new toplevel command
   - Example of function call to print a simple message
+  - Example of function call to print a simple warning
+  - Example of function call to raise a simple error to the user
   - Example of syntax to add a simple tactic
       (that does nothing and prints a message)
   - To use it:
@@ -54,19 +42,23 @@ make                        # build
     Require Import Tuto0.Loader. HelloWorld.
 ```
 
-  # tuto1 : Ocaml to Coq communication
+  You can also modify and run `theories/Demo.v`.
+
+  # 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 take arguments: strings, integers, symbols, expressions of the calculus of constructions
+  - Examples of using environments correctly
+  - Examples of using state (the evar_map) correctly
   - Commands that interact with type-checking in Coq
+  - A command that checks convertibility between two terms
   - 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 command that defines a new tactic
 
   Compilation and loading must be performed as for `tuto0`.
   
-  # tuto2 : Ocaml to Coq communication
+  # 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