From 003179e062bb7ae2c8169b0e4d3beddd87695afc Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 18 Mar 2025 14:00:32 +0100
Subject: [PATCH] link to TB readme

---
 README.md | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 0505dbb6..62659a41 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,7 @@
 # Simuliris Coq development
 
 This repository contains the Coq development of Simuliris (paper presented at POPL22: https://iris-project.org/pdfs/2022-popl-simuliris.pdf).
+It also contains the proofs for [Tree Borrows](theories/tree_borrows/README.md).
 
 ## Prerequisites
 
@@ -65,7 +66,7 @@ The project follows the following structure below the `theories` folder:
     * `adequacy.v` contains the resulting adequacy proof.
     * `examples` contains example optimizations, see below.
 - `tree_borrows` contains the Simuliris development of Tree Borrows.
-  This development has its own README in `tree_borrows/README.md`.
+  This development has its [own README](theories/tree_borrows/README.md).
 
 
 ## Theorems, definitions, and examples referenced in the paper
-- 
GitLab