package build carries menhir and rocq, docs completeness pass

4 files changed, 25 insertions, 1 deletions

diff --git a/README.org b/README.org
index 832ce9d..0592a66 100644
--- a/README.org
+++ b/README.org
@@ -71,9 +71,13 @@ It covers:
 - the catalog as ordinary queryable relations;
 - subtyping as proven relation inclusion, intensional relation
   identity, and canonical representatives for quotient domains;
+- OCaml for the implementation, Rocq for the proofs, extraction
+  binding the two;
 - applications as propositions everywhere: no relation application
   in term position, statements about results written flat as
-  membership.
+  membership;
+- relation references as a term kind, written =#Name=: relations as
+  data for transitions, higher-order arguments, and the catalog.
 
 ** Core Design Principles and Pipeline Specification
 
diff --git a/dune-project b/dune-project
index 4ba98c7..d490405 100644
--- a/dune-project
+++ b/dune-project
@@ -22,4 +22,5 @@
    (>= 5.1))
   zarith
   (menhir :build)
+  (coq :build)
   (alcotest :with-test)))
diff --git a/examples/README.org b/examples/README.org
index 20b853a..3ab427f 100644
--- a/examples/README.org
+++ b/examples/README.org
@@ -43,6 +43,15 @@ per line.
   bottom show facts that make admission reject the whole program;
   uncomment one and run again to see it happen.
 
+* What is not here
+
+States, transitions and commit (=[Insert relation: #Person ...]=,
+=at:= scoped reads, the branch tip) belong to the stateful world
+and do not exist in the standalone binary, by decision 5: standalone
+Sol is the pure fragment. The working demonstration of that half
+lives in =test/test_branch.ml=, driven through the embedding
+interface the way RNT drives it.
+
 * Reading the answers
 
 Each query prints one line per answer: variable bindings in Sol
diff --git a/flake.nix b/flake.nix
index 8a52938..bd1d2d2 100644
--- a/flake.nix
+++ b/flake.nix
@@ -26,6 +26,16 @@
             duneVersion = "3";
             src = self;
 
+            # The parser is menhir-generated, and the proven
+            # containment/lexicographic checkers are extracted from
+            # Rocq during the build.
+            nativeBuildInputs = [
+              ocamlPackages.menhir
+              pkgs.coq
+            ];
+            buildInputs = [
+              pkgs.coqPackages.stdlib
+            ];
             propagatedBuildInputs = [
               ocamlPackages.zarith
             ];