doclib

generator/Makefile

@@ -24,6 +24,8 @@ clean:
 # TODO: understand if myocamldeb is needed or not.
 
 
+#####################################################################
+
 doc: README.html
 
 README.html: README.md

lib/coq/Makefile

@@ -39,3 +39,11 @@ COQINCLUDE := -R $(CFML)/lib/tlc TLC -R . CFML
 include $(CFML)/lib/make/Makefile.coq
 
 quick_cf: CFHeader.vio
+
+
+#####################################################################
+
+doc: README.html
+
+README.html: README.md
+	pandoc -o $@ $<

lib/coq/README.md

+
+
+
+
+#####################################################################
+# Packaged libraries and compilation 
+
+`CFHeader.v`
+:    This file packages the scripts needed for compiling a `*_ml.v` file. Execute `make quick_cf` to build `CFHeader.vio` and be ready to compile a `*_ml.v` file.
+
+`CFLib.v`
+:    This file packages the scripts needed for compiling a `*_proof.v` file, using the CFML tactics. Execute `make quick` to be ready to compile a `*_proof.v` file.
+
+
+#####################################################################
+# Organization of the code
+
+`Shared.v`
+:    Contains general-purpose definition and tactics used in CFML.
+
+`CFHeaps.v`
+:    Contains the formalization of heaps and heap predicates. It also includes the definition of `local` and of tactics such as `hsimpl`.
+
+`CFApp.v`
+:    Contains an axiomatization of the behavior of ML function applications, as well as record operations.
+
+`CFPrint.v`
+:    Describes notation for pretty-printing characteristic formulae.
+
+`CFHeader.v`
+:    Packages the libraries used for compiling a `*_ml.v` file.
+
+`CFTactics.v`
+:    Contains the implementation of CFML tactics.
+
+`CFLib.v`
+:    Packages the libraries used for compiling a `*_proof.v` file.
+
+
+#####################################################################
+# For debugging
+
+`CFDemos.v`
+:    This file contains a bunch of unit tests.
+