From 8f12af876ed29ea7d05f7ec7c4f9a38a32be4386 Mon Sep 17 00:00:00 2001
From: Ralph Matthes <rmatthes@users.noreply.github.com>
Date: Fri, 4 Sep 2026 18:49:44 +0200
Subject: [PATCH] dune config from Coq to Rocq, not mentioning -type-in-type

---
 TypeTheory/dune | 12 ++++++++----
 dune-project    |  4 ++--
 2 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/TypeTheory/dune b/TypeTheory/dune
index 18329d96..a16775ff 100644
--- a/TypeTheory/dune
+++ b/TypeTheory/dune
@@ -1,7 +1,11 @@
 
 (include_subdirs qualified)
 
-(coq.theory
-  (name TypeTheory)
-  (flags -noinit -indices-matter -type-in-type -w none)
-  (theories UniMath))
+(rocq.theory
+ (name TypeTheory)
+ (flags :standard
+        -noinit
+        -indices-matter
+ ;;       -type-in-type
+	-w none)
+ (theories UniMath))
diff --git a/dune-project b/dune-project
index eafc3022..a7f07b80 100644
--- a/dune-project
+++ b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 3.8)
-(using coq 0.8)
+(lang dune 3.21)
+(using rocq 0.11)
 (name TypeTheory)