From 281fc90700926bd7eb80727bb9e752472d276ba2 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Tue, 8 May 2018 08:47:58 +0200 Subject: attempt to make code inclusions appear correctly --- README.md | 24 ++++++++++++++++++++---- 1 file changed, 20 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index a1ca482a5f..636fe265e0 100644 --- a/README.md +++ b/README.md @@ -2,18 +2,20 @@ How to write plugins in Coq =========================== # Working environment : merlin, tuareg (open question) # tuto0 : basics of project organization - * package a ml4 file in a plugin, organize a `Makefile`, `_CoqProject` + 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 -R theories Tuto0` +
+    cd tuto0; make
+    coqtop -I src -R theories Tuto0
+
In the Coq session type: `Require Tuto0.Loader. HelloWorld.` # tuto1 : Ocaml to Coq communication - * Explore the memory of Coq, modify it + Explore the memory of Coq, modify it - Commands that take arguments: strings, symbols, expressions of the calculus of constructions - Commands that interact with type-checking in Coq - A command that adds a new definition or theorem @@ -22,3 +24,17 @@ How to write plugins in Coq - A command that exploits an existing ongoing proof - A command that defines a new tactic + # 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 + - Handling commands that store information in user-chosen registers and tables + + + # tuto3 : manipulating terms of the calculus of constructions + obtaining existing values from memory and composing them, making sure + they are well-typed, and using them in new definitions and proofs. + - + + + \ No newline at end of file -- cgit v1.2.3