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))