From 481c1ac4c14522de8b2a4044fb82023a8a237cf8 Mon Sep 17 00:00:00 2001
From: Peter LeFanu Lumsdaine <p.l.lumsdaine@gmail.com>
Date: Wed, 10 Jun 2026 15:44:17 +0200
Subject: [PATCH] added minimal _RocqProject so that VSCode gets correct
 LoadPath for internal imports

---
 _RocqProject | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 _RocqProject

diff --git a/_RocqProject b/_RocqProject
new file mode 100644
index 00000000..5fa1fa8e
--- /dev/null
+++ b/_RocqProject
@@ -0,0 +1 @@
+-Q TypeTheory TypeTheory
\ No newline at end of file