aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYves Bertot2018-05-01 21:45:22 +0200
committerYves Bertot2018-05-01 21:45:22 +0200
commit3df17ed7972dc404cc8519ae9bfd42f75e278e0b (patch)
tree5f447e894f05ace71160451bb58af4dee7799af0
parent7ea3de67a88949c026f9715780f4fc3c5c5875f3 (diff)
add usage explanations
-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.`