From 257f5288a486740187e44b6ef4cadaad7166930e Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sun, 12 Jul 2026 18:15:31 -0300
Subject: package build carries menhir and rocq, docs completeness pass

---
 README.org | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'README.org')

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
 
-- 
cgit v1.2.3