From 44e8f6ee699ee07b66ebf134400f00e92feba491 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 7 Feb 2025 11:29:03 +0100
Subject: [PATCH] fix tests on < 9.0

---
 Makefile                                      | 43 ++++++----
 apps/derive/examples/usage.v                  |  1 -
 apps/derive/tests-stdlib/dune                 |  2 +-
 apps/derive/tests-stdlib/test_derive.v        |  4 -
 apps/eltac/tests-stdlib/dune                  |  2 +-
 apps/tc/tests-stdlib/bigTest.v                |  7 +-
 apps/tc/tests-stdlib/dune                     |  2 +-
 apps/tc/tests-stdlib/stdppInj.v               |  8 +-
 apps/tc/tests-stdlib/stdppInjClassic.v        |  8 +-
 apps/tc/tests-stdlib/test_import/f1.v         |  2 +-
 builtin-doc/coq-builtin.elpi                  |  7 --
 examples-stdlib/dune                          |  2 +-
 examples/dune                                 |  8 --
 ...tactic.v.in => tutorial_coq_elpi_tactic.v} |  3 +-
 tests-stdlib/dune                             |  2 +-
 tests-stdlib/test_API_env.v                   |  6 +-
 tests-stdlib/test_open_terms.v                |  3 +-
 tests-stdlib/test_quotation.v                 |  2 +-
 theories-stdlib/Arith.v.in                    |  3 +
 theories-stdlib/FunctionalExtensionality.v.in |  3 +
 theories-stdlib/List.v.in                     |  3 +
 theories-stdlib/Peano.v.in                    |  3 +
 theories-stdlib/Permutation.v.in              |  3 +
 theories-stdlib/Program/Basics.v.in           |  3 +
 theories-stdlib/Program/Syntax.v.in           |  3 +
 theories-stdlib/Program/dune                  | 15 ++++
 theories-stdlib/Ranalysis5.v.in               |  3 +
 theories-stdlib/Utf8.v.in                     |  3 +
 theories-stdlib/Vector.v.in                   |  3 +
 theories-stdlib/ZArith.v.in                   |  3 +
 theories-stdlib/dune.in                       | 79 +++++++++++++++++++
 31 files changed, 179 insertions(+), 60 deletions(-)
 rename examples/{tutorial_coq_elpi_tactic.v.in => tutorial_coq_elpi_tactic.v} (99%)
 create mode 100644 theories-stdlib/Arith.v.in
 create mode 100644 theories-stdlib/FunctionalExtensionality.v.in
 create mode 100644 theories-stdlib/List.v.in
 create mode 100644 theories-stdlib/Peano.v.in
 create mode 100644 theories-stdlib/Permutation.v.in
 create mode 100644 theories-stdlib/Program/Basics.v.in
 create mode 100644 theories-stdlib/Program/Syntax.v.in
 create mode 100644 theories-stdlib/Program/dune
 create mode 100644 theories-stdlib/Ranalysis5.v.in
 create mode 100644 theories-stdlib/Utf8.v.in
 create mode 100644 theories-stdlib/Vector.v.in
 create mode 100644 theories-stdlib/ZArith.v.in
 create mode 100644 theories-stdlib/dune.in

diff --git a/Makefile b/Makefile
index d268e8f33..e8ccca073 100644
--- a/Makefile
+++ b/Makefile
@@ -1,56 +1,65 @@
 dune = dune $(1) $(DUNE_$(1)_FLAGS)
 
-all:
+all: theories-stdlib/dune
 	$(call dune,build)
 	$(call dune,build) builtin-doc
 .PHONY: all
 
-build-core:
+build-core: theories-stdlib/dune
 	$(call dune,build) theories
 	$(call dune,build) builtin-doc
 .PHONY: build-core
 
-build-apps:
+build-apps: theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name theories)
 .PHONY: build-apps
 
-build:
+build: theories-stdlib/dune
 	$(call dune,build) -p coq-elpi @install
 	$(call dune,build) builtin-doc
 .PHONY: build
 
-test-core:
+all-tests: test-core test-stdlib test-apps test-apps-stdlib
+.PHONY: all-tests
+
+test-core: theories-stdlib/dune
 	$(call dune,runtest) tests
 	$(call dune,build) tests
 .PHONY: test-core
 
-test-apps:
+test-apps: theories-stdlib/dune
 	$(call dune,build) $$(find apps -type d -name tests)
 .PHONY: test-apps
 
-test-apps-stdlib:
+test-apps-stdlib: theories-stdlib/dune
 	$(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:
+test-stdlib: theories-stdlib/dune
 	$(call dune,build) tests-stdlib
-	$(call dune,build) $$(find apps -type d -name tests-stdlib)
 .PHONY: test-stdlib
 
-examples:
+all-examples: examples examples-stdlib
+.PHONY: all-examples
+
+examples: theories-stdlib/dune
 	$(call dune,build) examples
 .PHONY: examples
 
-examples-stdlib:
+examples-stdlib: theories-stdlib/dune
 	$(call dune,build) examples-stdlib
 .PHONY: examples-stdlib
 
+theories-stdlib/dune: theories-stdlib/dune.in
+	@rm -f $@
+	@echo "; generated by make, do not edit" > $@
+	@if $$(coqc --version | grep -q "8.19\|8.20") ; then \
+		sed -e 's/@@STDLIB@@//' $< >> $@ ; \
+	else \
+		sed -e 's/@@STDLIB@@/Stdlib/' $< >> $@ ; \
+	fi
+	@chmod a-w $@
+
 doc: build
 	@echo "########################## generating doc ##########################"
 	@mkdir -p doc
diff --git a/apps/derive/examples/usage.v b/apps/derive/examples/usage.v
index 42ec0bad8..629ad36b0 100644
--- a/apps/derive/examples/usage.v
+++ b/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.
 
diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune
index 4b33e1e32..2411d4773 100644
--- a/apps/derive/tests-stdlib/dune
+++ b/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)
diff --git a/apps/derive/tests-stdlib/test_derive.v b/apps/derive/tests-stdlib/test_derive.v
index 2d4fedeac..a4071e9d8 100644
--- a/apps/derive/tests-stdlib/test_derive.v
+++ b/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.
diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune
index e081ed767..8c31d8a88 100644
--- a/apps/eltac/tests-stdlib/dune
+++ b/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)
diff --git a/apps/tc/tests-stdlib/bigTest.v b/apps/tc/tests-stdlib/bigTest.v
index 2b483464b..ceb8c3cba 100644
--- a/apps/tc/tests-stdlib/bigTest.v
+++ b/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.
diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune
index 4ddf9df39..91824cb3d 100644
--- a/apps/tc/tests-stdlib/dune
+++ b/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)
diff --git a/apps/tc/tests-stdlib/stdppInj.v b/apps/tc/tests-stdlib/stdppInj.v
index 2407f771b..6732fce2e 100644
--- a/apps/tc/tests-stdlib/stdppInj.v
+++ b/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.
diff --git a/apps/tc/tests-stdlib/stdppInjClassic.v b/apps/tc/tests-stdlib/stdppInjClassic.v
index 1bc27ad74..d9d4e9551 100644
--- a/apps/tc/tests-stdlib/stdppInjClassic.v
+++ b/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.
diff --git a/apps/tc/tests-stdlib/test_import/f1.v b/apps/tc/tests-stdlib/test_import/f1.v
index de8f271bc..40ad764d6 100644
--- a/apps/tc/tests-stdlib/test_import/f1.v
+++ b/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.
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
index 4d62b1f8b..3646a03b4 100644
--- a/builtin-doc/coq-builtin.elpi
+++ b/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.
diff --git a/examples-stdlib/dune b/examples-stdlib/dune
index bbdbedb9f..96a3ac4b8 100644
--- a/examples-stdlib/dune
+++ b/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)
diff --git a/examples/dune b/examples/dune
index eb40f9ac5..9a7bee3cd 100644
--- a/examples/dune
+++ b/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)
diff --git a/examples/tutorial_coq_elpi_tactic.v.in b/examples/tutorial_coq_elpi_tactic.v
similarity index 99%
rename from examples/tutorial_coq_elpi_tactic.v.in
rename to examples/tutorial_coq_elpi_tactic.v
index 114bd36a0..a070cd55e 100644
--- a/examples/tutorial_coq_elpi_tactic.v.in
+++ b/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 *)
diff --git a/tests-stdlib/dune b/tests-stdlib/dune
index 405ac7369..3793ba99d 100644
--- a/tests-stdlib/dune
+++ b/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)
diff --git a/tests-stdlib/test_API_env.v b/tests-stdlib/test_API_env.v
index 2d1f4391a..d60655fdb 100644
--- a/tests-stdlib/test_API_env.v
+++ b/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,
diff --git a/tests-stdlib/test_open_terms.v b/tests-stdlib/test_open_terms.v
index a15cfc780..3600951e1 100644
--- a/tests-stdlib/test_open_terms.v
+++ b/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.
diff --git a/tests-stdlib/test_quotation.v b/tests-stdlib/test_quotation.v
index c11c018d6..e4cef5ec7 100644
--- a/tests-stdlib/test_quotation.v
+++ b/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 =>
diff --git a/theories-stdlib/Arith.v.in b/theories-stdlib/Arith.v.in
new file mode 100644
index 000000000..04920cbde
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/FunctionalExtensionality.v.in b/theories-stdlib/FunctionalExtensionality.v.in
new file mode 100644
index 000000000..63a2e73ef
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/List.v.in b/theories-stdlib/List.v.in
new file mode 100644
index 000000000..190fe8031
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Peano.v.in b/theories-stdlib/Peano.v.in
new file mode 100644
index 000000000..291744c89
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Permutation.v.in b/theories-stdlib/Permutation.v.in
new file mode 100644
index 000000000..7f221d6da
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Program/Basics.v.in b/theories-stdlib/Program/Basics.v.in
new file mode 100644
index 000000000..d5ebbebd3
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Program/Syntax.v.in b/theories-stdlib/Program/Syntax.v.in
new file mode 100644
index 000000000..d3228e5ab
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Program/dune b/theories-stdlib/Program/dune
new file mode 100644
index 000000000..5d2f6304e
--- /dev/null
+++ b/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}))))
\ No newline at end of file
diff --git a/theories-stdlib/Ranalysis5.v.in b/theories-stdlib/Ranalysis5.v.in
new file mode 100644
index 000000000..174608623
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Utf8.v.in b/theories-stdlib/Utf8.v.in
new file mode 100644
index 000000000..2a760eeb6
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/Vector.v.in b/theories-stdlib/Vector.v.in
new file mode 100644
index 000000000..6a43407f1
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/ZArith.v.in b/theories-stdlib/ZArith.v.in
new file mode 100644
index 000000000..30b96df26
--- /dev/null
+++ b/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.
+
diff --git a/theories-stdlib/dune.in b/theories-stdlib/dune.in
new file mode 100644
index 000000000..a86c650ba
--- /dev/null
+++ b/theories-stdlib/dune.in
@@ -0,0 +1,79 @@
+(coq.theory
+ (name elpi_stdlib)
+ (plugins coq-elpi.elpi)
+ (package coq-elpi-tests-stdlib)
+ (theories elpi_elpi elpi @@STDLIB@@))
+
+(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)
\ No newline at end of file