From 334ec6e9bbf67a88d113f10170678a888179f113 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 10 Apr 2026 12:52:11 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/stdlib/pull/251 --- examples/dune | 2 +- test-suite/dune | 2 +- theories/Prop/dune | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/examples/dune b/examples/dune index 45db7c6d..49e48a63 100644 --- a/examples/dune +++ b/examples/dune @@ -5,6 +5,6 @@ (synopsis "Equations Plugin Examples") (plugins rocq-runtime.plugins.extraction rocq-equations.plugin) (modules :standard \ IdDec NoCycle) - (theories Stdlib Equations Equations.Prop Equations.Type)) + (theories micromega_plugin Stdlib Equations Equations.Prop Equations.Type)) ; we need micromega_plugin because dune is unfortunately unable to handle transitive dependencies (include_subdirs no) \ No newline at end of file diff --git a/test-suite/dune b/test-suite/dune index b15d5418..3ed3e75d 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -4,6 +4,6 @@ (package rocq-equations-tests) (synopsis "Equations Plugin Tests") (plugins rocq-runtime.plugins.extraction) - (theories Stdlib Equations Equations.Prop Equations.Type)) + (theories micromega_plugin Stdlib Equations Equations.Prop Equations.Type)) ; we need micromega_plugin because dune is unfortunately unable to handle transitive dependencies (include_subdirs no) diff --git a/theories/Prop/dune b/theories/Prop/dune index ff5302fe..830b4aaa 100644 --- a/theories/Prop/dune +++ b/theories/Prop/dune @@ -3,5 +3,5 @@ (name Equations.Prop) (package rocq-equations) (synopsis "Equations Plugin") - (theories Stdlib Equations) + (theories micromega_plugin Stdlib Equations) ; we need micromega_plugin because dune is unfortunately unable to handle transitive dependencies (modules :standard))