aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md7
1 files changed, 6 insertions, 1 deletions
diff --git a/README.md b/README.md
index 568a56bf37..d6100c8a75 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,12 @@
How to write plugins in Coq
===========================
- * tuto0 : package a ml4 file in a plugin, organize a Makefile, _CoqProject
+ * tuto0 : 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.
+ To use it:
+ `cd tuto0; make`
+ `coqtop -I src`
+
+ Dans la session Coq, taper `Require ML Module "tuto0_plugin". HelloWorld.`