diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune index 147d5c92c..49fcebd04 100644 --- a/apps/derive/tests-stdlib/dune +++ b/apps/derive/tests-stdlib/dune @@ -2,6 +2,6 @@ (package rocq-elpi-tests-stdlib) (name elpi_apps_derive_tests_stdlib) (flags :standard -w -default-output-directory) - (theories elpi elpi.apps.derive elpi.apps.derive.tests Stdlib)) + (theories elpi elpi.apps.derive elpi.apps.derive.tests micromega_plugin Stdlib)) ; we need micromega_plugin because dune doesn't handle transitive dependencies (include_subdirs qualified) diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune index 73a8c7cfb..4832c845c 100644 --- a/apps/eltac/tests-stdlib/dune +++ b/apps/eltac/tests-stdlib/dune @@ -1,6 +1,6 @@ (coq.theory (package rocq-elpi-tests-stdlib) (name elpi_apps_eltac_tests_stdlib) - (theories elpi elpi.apps.eltac Stdlib)) + (theories elpi elpi.apps.eltac micromega_plugin Stdlib)) ; we need micromega_plugin because dune doesn't handle transitive dependencies (include_subdirs qualified) diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune index fb351e464..29273b0a7 100644 --- a/apps/tc/tests-stdlib/dune +++ b/apps/tc/tests-stdlib/dune @@ -2,6 +2,6 @@ (package rocq-elpi-tests-stdlib) (name elpi_apps_tc_tests_stdlib) (flags :standard -async-proofs-cache force) - (theories elpi elpi.apps.tc elpi.apps.tc.tests Stdlib)) + (theories elpi elpi.apps.tc elpi.apps.tc.tests micromega_plugin Stdlib)) ; we need micromega_plugin because dune doesn't handle transitive dependencies (include_subdirs qualified) diff --git a/examples-stdlib/dune b/examples-stdlib/dune index ec9aa161b..77bf598db 100644 --- a/examples-stdlib/dune +++ b/examples-stdlib/dune @@ -2,6 +2,6 @@ (package rocq-elpi-tests-stdlib) (name elpi_examples_stdlib) (plugins rocq-elpi.elpi) - (theories elpi Stdlib)) + (theories elpi micromega_plugin Stdlib)) ; we need micromega_plugin because dune doesn't handle transitive dependencies ; (include_subdirs qualified) diff --git a/tests-stdlib/dune b/tests-stdlib/dune index 00c0b019b..85554da6f 100644 --- a/tests-stdlib/dune +++ b/tests-stdlib/dune @@ -2,6 +2,6 @@ (package rocq-elpi-tests-stdlib) (name elpi_tests_stdlib) (plugins rocq-elpi.elpi) - (theories elpi Stdlib)) + (theories elpi micromega_plugin Stdlib)) ; we need micromega_plugin because dune doesn't handle transitive dependencies ; (include_subdirs qualified) diff --git a/tests-stdlib/test_ring.v b/tests-stdlib/test_ring.v index 36bc54c59..df6bf5ebf 100644 --- a/tests-stdlib/test_ring.v +++ b/tests-stdlib/test_ring.v @@ -3,12 +3,12 @@ From Stdlib Require Import ZArith Lia. (* we test we can call ML tactics *) -Elpi Tactic xlia. +Elpi Tactic mp_lia. Elpi Accumulate lp:{{ - solve G GL :- coq.ltac.call-mltac "rocq-runtime.plugins.micromega" "Lia" 0 G GL ok. + solve G GL :- coq.ltac.call-mltac "micromega-plugin.plugin" "Lia" 0 G GL ok. }}. Tactic Notation "mylia" := - Zify.zify; elpi xlia ltac_tactic:(zchecker). + Zify.zify; elpi mp_lia ltac_tactic:(zchecker). Open Scope Z.