Make make work on 9.0

LPCIC · Feb 7, 2025 · 219b475 · 219b475
1 parent 65655e0
commit 219b475
Show file tree

Hide file tree

Showing 8 changed files with 26 additions and 8 deletions.
diff --git a/apps/tc/examples/dune b/apps/tc/examples/dune
@@ -1,5 +1,5 @@
 (coq.theory
  (name elpi.apps.tc.examples)
- (theories elpi elpi.apps.tc))
+ (theories elpi elpi.apps.tc elpi_stdlib))
 
 (include_subdirs qualified)
diff --git a/apps/tc/examples/tutorial.v b/apps/tc/examples/tutorial.v
@@ -1,4 +1,4 @@
-Require Import Bool.
+From elpi_stdlib Require Import Bool.
 From elpi.apps Require Import tc.
 
 Class Eqb (T: Type) := {
@@ -93,4 +93,5 @@ Module Backtrack.
 End Backtrack.
 
 TC.Print_instances.
-TC.Get_class_info DecidableClass.Decidable.
+(* Require Stdlib *)
+(* TC.Get_class_info DecidableClass.Decidable. *)
diff --git a/apps/tc/tests-stdlib/bigTest.v b/apps/tc/tests-stdlib/bigTest.v
@@ -12,7 +12,7 @@ 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 elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid.
-From elpi_stdlib Require Export Peano Utf8 Permutation.
+From elpi_stdlib Require Export Bool List Peano Utf8 Permutation.
 From elpi_stdlib Require Export Program.Basics Program.Syntax.
 
 Export ListNotations.

diff --git a/apps/tc/tests-stdlib/stdppInj.v b/apps/tc/tests-stdlib/stdppInj.v
@@ -1,7 +1,7 @@
 (* Test inspired from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/base.v *)
 
 From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid.
-From elpi_stdlib Require Export Peano Utf8 Permutation.
+From elpi_stdlib Require Export List Peano Utf8 Permutation.
 From elpi_stdlib Require Export Program.Basics Program.Syntax.
 
 Export ListNotations.
@@ -265,4 +265,4 @@ Qed.
 
 Goal Inj eq eq (fun (x: nat) => (compose id id) (id x)).
 apply (compose_inj eq eq); apply _.
-Qed.
+Qed.
diff --git a/apps/tc/tests-stdlib/stdppInjClassic.v b/apps/tc/tests-stdlib/stdppInjClassic.v
@@ -1,6 +1,6 @@
 (* File inspired from https://gitlab.mpi-sws.org/iris/stdpp/-/blob/8c98553ad0ca2029b30cf18b58e321ec3a79172b/stdpp/base.v *)
 From elpi.core Require Export Morphisms RelationClasses ListDef Bool Setoid.
-From elpi_stdlib Require Export Peano Utf8 Permutation.
+From elpi_stdlib Require Export List Peano Utf8 Permutation.
 From elpi_stdlib Require Export Program.Basics Program.Syntax.
 
 Export ListNotations.
@@ -218,4 +218,4 @@ Qed. *)
 
 Goal Inj eq eq (fun (x: nat) => (compose id id) (id x)).
 apply (compose_inj eq eq); apply _.
-Qed.
+Qed.
diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi
@@ -1372,6 +1372,13 @@ 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/theories-stdlib/Bool.v.in b/theories-stdlib/Bool.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export Bool.
+#[skip="8.20"] From Stdlib Require Export Bool.
diff --git a/theories-stdlib/dune.in b/theories-stdlib/dune.in
@@ -4,6 +4,14 @@
  (package coq-elpi-tests-stdlib)
  (theories elpi_elpi elpi @@STDLIB@@))
 
+(rule
+ (target Bool.v)
+ (deps
+  (glob_files Bool.v.in))
+ (action
+  (with-stdout-to %{target}
+   (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps}))))
+
 (rule
  (target Vector.v)
  (deps
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,2 @@
		#[only="8.20"] From Coq Require Export Bool.
		#[skip="8.20"] From Stdlib Require Export Bool.