From 5518d45cc2d4bc0c9fb63da286041b44f8c69c22 Mon Sep 17 00:00:00 2001
From: Gregory Malecha <gregory@skylabs-ai.com>
Date: Fri, 22 May 2026 21:55:47 -0400
Subject: [PATCH] Transitive dependencies for floating point

---
 rocq-brick-libstdcpp/proof/dune | 24 ++++++++++++++++--------
 rocq-brick-libstdcpp/test/dune  | 24 ++++++++++++++++--------
 2 files changed, 32 insertions(+), 16 deletions(-)

diff --git a/rocq-brick-libstdcpp/proof/dune b/rocq-brick-libstdcpp/proof/dune
index c388151..72e0f3d 100644
--- a/rocq-brick-libstdcpp/proof/dune
+++ b/rocq-brick-libstdcpp/proof/dune
@@ -5,27 +5,35 @@
  (name skylabs.brick.libstdcpp) ; logical path of this library
  (package rocq-brick-libstdcpp)
  (theories
-  ; skylabs deps
   Stdlib
   stdpp
   skylabs.upoly
-  elpi elpi_elpi elpi.apps.locker elpi.apps.NES
-  Lens Lens.Elpi
-  Ltac2 skylabs.ltac2.extra
+  elpi
+  elpi_elpi
+  elpi.apps.locker
+  elpi.apps.NES
+  Lens
+  Lens.Elpi
+  Ltac2
+  skylabs.ltac2.extra
   skylabs.prelude
   iris
   skylabs.iris.extra
-  Equations Equations.Prop Equations.Type
+  Equations
+  Equations.Prop
+  Equations.Type
   skylabs.lang.cpp
   skylabs.ltac2.logger
   skylabs.auto.core
-  ;
   ExtLib
   skylabs.elpi.extra
   skylabs.elpi.cpp
   tactic_classes
-  ; skylabs deps end
-  skylabs))
+  skylabs
+  ; transitive dependencies
+  Corelib Flocq elpi.apps.NES.elpi elpi.apps.derive elpi.apps.derive.elpi
+  elpi.apps.locker.elpi
+ ))
 (include dune.inc)
 
 (rule
diff --git a/rocq-brick-libstdcpp/test/dune b/rocq-brick-libstdcpp/test/dune
index fc9ecc5..e8226d0 100644
--- a/rocq-brick-libstdcpp/test/dune
+++ b/rocq-brick-libstdcpp/test/dune
@@ -4,28 +4,36 @@
 (rocq.theory
  (name skylabs.brick.libstdcpp.test) ; logical path of this library
  (theories
-  ; skylabs.brick.libstdcpp deps
   Stdlib
   stdpp
   skylabs.upoly
-  elpi elpi_elpi elpi.apps.locker elpi.apps.NES
-  Lens Lens.Elpi
-  Ltac2 skylabs.ltac2.extra
+  elpi
+  elpi_elpi
+  elpi.apps.locker
+  elpi.apps.NES
+  Lens
+  Lens.Elpi
+  Ltac2
+  skylabs.ltac2.extra
   skylabs.prelude
   iris
   skylabs.iris.extra
-  Equations Equations.Prop Equations.Type
+  Equations
+  Equations.Prop
+  Equations.Type
   skylabs.lang.cpp
   skylabs.ltac2.logger
   skylabs.auto.core
-  ;
   ExtLib
   skylabs.elpi.extra
   skylabs.elpi.cpp
   skylabs
   tactic_classes
-  ; skylabs.brick.libstdcpp deps end
-  skylabs.brick.libstdcpp))
+  skylabs.brick.libstdcpp
+  ; transitive dependencies
+  Corelib Flocq elpi.apps.NES.elpi elpi.apps.derive elpi.apps.derive.elpi
+  elpi.apps.locker.elpi
+ ))
 (include dune.inc)
 
 (rule