aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorYves Bertot2018-05-01 21:34:48 +0200
committerYves Bertot2018-05-01 21:34:48 +0200
commit7ea3de67a88949c026f9715780f4fc3c5c5875f3 (patch)
treeb5b34b3b885959da0d396f00670a1c419f502918
parentb5c0be9687aad69913e24354a041f188ee25efaf (diff)
add a simple explanation in the README file
-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.
+