fix tests on < 9.0

Makefile

@@ -19,6 +19,9 @@ build:
 	$(call dune,build) builtin-doc
 .PHONY: build
 
+all-tests: test-core test-stdlib test-apps test-apps-stdlib
+.PHONY: all-tests
+
 test-core:
 	$(call dune,runtest) tests
 	$(call dune,build) tests
@@ -32,17 +35,13 @@ test-apps-stdlib:
 	$(call dune,build) $$(find apps -type d -name tests-stdlib)
 .PHONY: test-apps-stdlib
 
-test:
-	$(call dune,runtest)
-	$(call dune,build) tests
-	$(call dune,build) $$(find apps -type d -name tests)
-.PHONY: test
-
 test-stdlib:
 	$(call dune,build) tests-stdlib
-	$(call dune,build) $$(find apps -type d -name tests-stdlib)
 .PHONY: test-stdlib
 
+all-examples: examples examples-stdlib
+.PHONY: all-examples
+
 examples:
 	$(call dune,build) examples
 .PHONY: examples

apps/derive/examples/usage.v

@@ -2,7 +2,6 @@
    This example shows how to use derive
 *)
 
-From Coq Require Import Bool.
 From elpi.apps Require Import derive.std.
 Set Uniform Inductive Parameters.
 

apps/derive/tests-stdlib/dune

@@ -2,6 +2,6 @@
  (package coq-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 elpi_stdlib))
 
 (include_subdirs qualified)

apps/derive/tests-stdlib/test_derive.v

@@ -170,7 +170,3 @@ End derive_container.
 About wimpls.wimpls.
 About wimpls.Kwi.
 Redirect "tmp" Check Kwi _ (refl_equal 3).
-
-From Coq Require Ascii.
-
-#[only(param2)] derive Ascii.ascii.

apps/eltac/tests-stdlib/dune

@@ -1,6 +1,6 @@
 (coq.theory
  (package coq-elpi-tests-stdlib)
  (name elpi_apps_eltac_tests_stdlib)
- (theories elpi elpi.apps.eltac Stdlib))
+ (theories elpi elpi.apps.eltac elpi_stdlib))
 
 (include_subdirs qualified)

apps/tc/tests-stdlib/bigTest.v

@@ -11,10 +11,11 @@ These two functions being defined both in [Coq.Bool] and in [Coq.Peano],
 we must export [Coq.Peano] later than any export of [Coq.Bool]. *)
 (* We also want to ensure that notations from [Coq.Utf8] take precedence
 over the ones of [Coq.Peano] (see Coq PR#12950), so we import [Utf8] last. *)
-From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
-From Coq Require Import Permutation.
+From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid.
+From elpi_stdlib Require Export Peano Utf8 Permutation.
+From elpi_stdlib Require Export Program.Basics Program.Syntax.
+
 Export ListNotations.
-From Coq.Program Require Export Basics Syntax.
 
 TC.AddAllClasses.
 TC.AddAllInstances.

apps/tc/tests-stdlib/dune

@@ -2,6 +2,6 @@
  (package coq-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 elpi_stdlib))
 
 (include_subdirs qualified)

apps/tc/tests-stdlib/stdppInj.v

@@ -1,9 +1,11 @@
 (* Test inspired from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/base.v *)
 
-From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
-From Coq Require Import Permutation.
+From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid.
+From elpi_stdlib Require Export Peano Utf8 Permutation.
+From elpi_stdlib Require Export Program.Basics Program.Syntax.
+
 Export ListNotations.
-From Coq.Program Require Export Basics Syntax.
+
 
 From elpi.apps Require Import tc.
 Elpi TC Solver Override TC.Solver All.

apps/tc/tests-stdlib/stdppInjClassic.v

@@ -1,8 +1,10 @@
 (* File inspired from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/base.v *)
-From Coq Require Export Morphisms RelationClasses List Bool Setoid Peano Utf8.
-From Coq Require Import Permutation.
+From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid.
+From elpi_stdlib Require Export Peano Utf8 Permutation.
+From elpi_stdlib Require Export Program.Basics Program.Syntax.
+
 Export ListNotations.
-From Coq.Program Require Export Basics Syntax.
+
 
 Notation length := Datatypes.length.
 Global Generalizable All Variables.

apps/tc/tests-stdlib/test_import/f1.v

@@ -1,4 +1,4 @@
 From elpi.apps Require Export tc.
-From Coq Require Export Morphisms.
+From elpi.core Require Export Morphisms.
 
 Elpi TC Solver Override TC.Solver Rm Proper ProperProxy.

builtin-doc/coq-builtin.elpi

@@ -1372,13 +1372,6 @@ external pred coq.arguments.simplification i:gref,
 external pred coq.arguments.set-simplification i:gref, 
                                                i:simplification_strategy.
 
-% [coq.arguments.reset-simplification GR] resets the behavior of the
-% simplification tactics.
-% Also resets the ! and / modifiers for the Arguments command.
-% Supported attributes:
-% - @global! (default: false)
-external pred coq.arguments.reset-simplification i:gref.
-
 % [coq.locate-abbreviation Name Abbreviation] locates an abbreviation.  It's
 % a fatal error if Name cannot be located.
 external pred coq.locate-abbreviation i:id, o:abbreviation.

examples-stdlib/dune

@@ -2,6 +2,6 @@
  (package coq-elpi-tests-stdlib)
  (name elpi_examples_stdlib)
  (plugins coq-elpi.elpi)
- (theories elpi Stdlib))
+ (theories elpi elpi_stdlib))
 
 ; (include_subdirs qualified)

examples/dune

@@ -4,12 +4,4 @@
  (plugins coq-elpi.elpi)
  (theories elpi))
 
-(rule
- (target tutorial_coq_elpi_tactic.v)
- (deps
-  (glob_files tutorial_coq_elpi_tactic.v.in))
- (action
-  (with-stdout-to %{target}
-   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
-
 ; (include_subdirs qualified)

examples/tutorial_coq_elpi_tactic.v.in → examples/tutorial_coq_elpi_tactic.v

@@ -1042,8 +1042,7 @@ Elpi Accumulate default lp:{{
 }}.
 
 
-#[only="8.20"] From Coq Require Import Uint63.
-#[skip="8.20"] From Corelib Require Import PrimInt63.
+From elpi.core Require Import PrimInt63.
 Open Scope uint63_scope.
 
 Fail Definition baz : list nat := default 1.  (* .fails *)

tests-stdlib/dune

@@ -2,6 +2,6 @@
  (package coq-elpi-tests-stdlib)
  (name elpi_tests_stdlib)
  (plugins coq-elpi.elpi)
- (theories elpi Stdlib))
+ (theories elpi elpi_stdlib))
 
 ; (include_subdirs qualified)

tests-stdlib/test_API_env.v

@@ -1,5 +1,5 @@
 From elpi Require Import elpi.
-From Coq Require Vector.
+From elpi_stdlib Require Vector.
 
 (****** env **********************************)
 Elpi Command test.
@@ -333,7 +333,7 @@ Elpi Query lp:{{
 
 End HOAS.
 
-From Coq Require Ranalysis5.
+From elpi_stdlib Require Ranalysis5.
 
 Elpi Query lp:{{
 
@@ -372,7 +372,7 @@ Elpi Query lp:{{
 Set Printing Universes. Print Module Test.
 Check Test.f.
 
-From Coq Require Import ZArith.
+From elpi_stdlib Require Import ZArith.
 
 Elpi Query lp:{{
   coq.locate-module "N2Z" MP,

tests-stdlib/test_open_terms.v

@@ -1,6 +1,5 @@
-Require Import Arith List FunctionalExtensionality.
+From elpi_stdlib Require Import ZArith Arith List FunctionalExtensionality.
 From elpi Require Import elpi.
-Require Import ZArith.
 
 Lemma ring_example x : x + 1 = 1 + x.
 Proof. ring. Qed.

tests-stdlib/test_quotation.v

@@ -29,7 +29,7 @@ Elpi Query lp:{{
   coq.say BO1.
 }}.
 
-Require Vector.
+From elpi_stdlib Require Vector.
 
 Elpi Query lp:{{
   T = {{ fun v : Vector.t nat 2 =>

theories-stdlib/Arith.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export Arith.
+#[skip="8.20"] From Stdlib Require Export Arith.
+

theories-stdlib/FunctionalExtensionality.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export FunctionalExtensionality.
+#[skip="8.20"] From Stdlib Require Export FunctionalExtensionality.
+

theories-stdlib/List.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export List.
+#[skip="8.20"] From Stdlib Require Export List.
+

theories-stdlib/Peano.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export Peano.
+#[skip="8.20"] From Stdlib Require Export Peano.
+

theories-stdlib/Permutation.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export Permutation.
+#[skip="8.20"] From Stdlib Require Export Permutation.
+

theories-stdlib/Program/Basics.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq.Program Require Export Basics.
+#[skip="8.20"] From Stdlib.Program Require Export Basics.
+

theories-stdlib/Program/Syntax.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq.Program Require Export Syntax.
+#[skip="8.20"] From Stdlib.Program Require Export Syntax.
+

theories-stdlib/Program/dune

@@ -0,0 +1,15 @@
+(rule
+ (target Basics.v)
+ (deps
+  (glob_files Basics.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target Syntax.v)
+ (deps
+  (glob_files Syntax.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))

theories-stdlib/Ranalysis5.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export Ranalysis5.
+#[skip="8.20"] From Stdlib Require Export Ranalysis5.
+

theories-stdlib/Utf8.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export Utf8.
+#[skip="8.20"] From Stdlib Require Export Utf8.
+

theories-stdlib/Vector.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export Vector.
+#[skip="8.20"] From Stdlib Require Export Vector.
+

theories-stdlib/ZArith.v.in

@@ -0,0 +1,3 @@
+#[only="8.20"] From Coq Require Export ZArith.
+#[skip="8.20"] From Stdlib Require Export ZArith.
+

theories-stdlib/dune

@@ -0,0 +1,79 @@
+(coq.theory
+ (name elpi_stdlib)
+ (plugins coq-elpi.elpi)
+ (package coq-elpi-tests-stdlib)
+ (theories elpi_elpi elpi))
+
+(rule
+ (target Vector.v)
+ (deps
+  (glob_files Vector.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target Arith.v)
+ (deps
+  (glob_files Arith.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target ZArith.v)
+ (deps
+  (glob_files ZArith.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target FunctionalExtensionality.v)
+ (deps
+  (glob_files FunctionalExtensionality.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target List.v)
+ (deps
+  (glob_files List.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target Ranalysis5.v)
+ (deps
+  (glob_files Ranalysis5.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target Utf8.v)
+ (deps
+  (glob_files Utf8.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target Peano.v)
+ (deps
+  (glob_files Peano.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(rule
+ (target Permutation.v)
+ (deps
+  (glob_files Permutation.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
+(include_subdirs qualified)