aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--README.md7
1 files changed, 7 insertions, 0 deletions
diff --git a/README.md b/README.md
new file mode 100644
index 0000000000..568a56bf37
--- /dev/null
+++ b/README.md
@@ -0,0 +1,7 @@
+How to write plugins in Coq
+===========================
+
+ * 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.
+