Remove unused Stdlib dependencies in tests

proux01 · proux01 · commit de9bba291aee · 2025-02-07T14:37:33.000+01:00
diff --git a/apps/coercion/tests/test.v b/apps/coercion/tests/test.v
@@ -1,6 +1,5 @@
 From elpi.apps Require Import coercion.
 #[warning="-deprecated-from-Coq"]
-From Coq Require Import Bool.
 
 Elpi Accumulate coercion.db lp:{{
 
@@ -9,7 +8,7 @@ coercion _ {{ False }} {{ Prop }} {{ bool }} {{ false }}.
 
 }}.
 
-Check True && False.
+Check andb True False.
 
 Parameter ringType : Type.
 Parameter ringType_sort : ringType -> Type.
diff --git a/apps/coercion/tests/test_open.v b/apps/coercion/tests/test_open.v
@@ -1,8 +1,7 @@
 From elpi.apps Require Import coercion.
-#[warning="-deprecated-from-Coq"]
-From Coq Require Import Arith ssreflect.
+From elpi.core Require Import ssreflect.
 
-Ltac my_solver := trivial with arith.
+Ltac my_solver := try ((repeat apply: le_n_S); apply: le_0_n).
 
 Elpi Accumulate coercion lp:{{
 
diff --git 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/test_bcongr.v b/apps/derive/tests/test_bcongr.v
@@ -1,3 +1,4 @@
+From elpi.core Require Import Bool.
 From elpi.apps Require Import derive.bcongr.
 
 From elpi.apps Require Import test_derive_corelib test_projK.
diff --git a/apps/derive/tests/test_derive_corelib.v b/apps/derive/tests/test_derive_corelib.v
@@ -1,6 +1,6 @@
 (* Some standard data types using different features *)
-From Coq Require Uint63.
-From Coq Require Floats.
+From elpi.core Require PrimInt63.
+From elpi.core Require PrimFloat.
 
 Module Coverage.
 
@@ -68,7 +68,7 @@ Inductive large :=
 | K25(_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) 
 | K26(_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit) (_ : unit).
 
-Inductive prim_int := PI (i : Uint63.int).
+Inductive prim_int := PI (i : PrimInt63.int).
 Inductive prim_float := PF (f : PrimFloat.float).
 
 Record fo_record := { f1 : peano; f2 : unit; }.
diff --git a/apps/derive/tests/test_eqb.v b/apps/derive/tests/test_eqb.v
@@ -41,7 +41,7 @@ Elpi derive.eqb alias.
 
 End Coverage.
 Import Coverage.
-Import PArith.
+From elpi.core Require Import PosDef.
 
 Notation eq_test T := (T -> T -> bool).
 Notation eq_test2 T1 T2 := (T1 -> T2 -> bool).
diff --git a/apps/derive/tests/test_eqbOK.v b/apps/derive/tests/test_eqbOK.v
@@ -1,3 +1,4 @@
+From elpi.core Require Import Bool.
 From elpi.apps Require Import derive.eqbOK.
 
 From elpi.apps.derive.tests Require Import test_derive_corelib test_eqb test_eqbcorrect.
@@ -48,7 +49,7 @@ End Coverage.
 
 Import Coverage.
 
-Redirect "tmp" Check peano_eqb_OK : forall n m, Bool.reflect (n = m) (peano_eqb n m).
-Redirect "tmp" Check seq_eqb_OK : forall A eqA (h : forall a1 a2 : A, Bool.reflect (a1 = a2) (eqA a1 a2)) l1 l2, Bool.reflect (l1 = l2) (seq_eqb A eqA l1 l2).
-Redirect "tmp" Check ord_eqb_OK : forall n (o1 o2 : ord n), Bool.reflect (o1 = o2) (ord_eqb n n o1 o2).
-Redirect "tmp" Check alias_eqb_OK : forall x y : alias, Bool.reflect (x = y) (alias_eqb x y).
+Redirect "tmp" Check peano_eqb_OK : forall n m, Datatypes.reflect (n = m) (peano_eqb n m).
+Redirect "tmp" Check seq_eqb_OK : forall A eqA (h : forall a1 a2 : A, Datatypes.reflect (a1 = a2) (eqA a1 a2)) l1 l2, Datatypes.reflect (l1 = l2) (seq_eqb A eqA l1 l2).
+Redirect "tmp" Check ord_eqb_OK : forall n (o1 o2 : ord n), Datatypes.reflect (o1 = o2) (ord_eqb n n o1 o2).
+Redirect "tmp" Check alias_eqb_OK : forall x y : alias, Datatypes.reflect (x = y) (alias_eqb x y).
diff --git a/apps/derive/tests/test_fields.v b/apps/derive/tests/test_fields.v
@@ -38,7 +38,7 @@ Elpi derive.fields val.
 End Coverage.
 
 Import Coverage.
-Import PArith.
+From elpi.core Require Import PosDef.
 
 Redirect "tmp" Check empty_fields_t : positive -> Type. 
 Redirect "tmp" Check empty_fields : forall (n:empty), empty_fields_t (empty_tag n). 
diff --git a/apps/derive/tests/test_tag.v b/apps/derive/tests/test_tag.v
@@ -39,7 +39,7 @@ Elpi derive.tag val.
 End Coverage.
 
 Import Coverage.
-Import PArith.
+From elpi.core Require Import PosDef.
 
 Local Notation tag X := (X -> positive).
 
diff --git a/apps/eltac/tests/test_apply.v b/apps/eltac/tests/test_apply.v
@@ -5,7 +5,9 @@ Proof.
     eltac.apply H.
 Qed.
 
+Axiom add_comm : forall x y, x + y = y + x.
+
 Goal (3 + 4 = 4 + 3).
 Proof.
-    eltac.apply PeanoNat.Nat.add_comm.
-Qed.
+    eltac.apply add_comm.
+Qed.
diff --git a/apps/eltac/tests/test_rewrite.v b/apps/eltac/tests/test_rewrite.v
@@ -1,12 +1,15 @@
 From elpi.apps Require Import eltac.rewrite.
 
+Axiom add_comm : forall x y, x + y = y + x.
+Axiom mul_comm : forall x y, x * y = y * x.
+
 Goal (forall x : nat, 1 + x = x + 1) -> 
     forall y,  2 * ((y+y) + 1) = ((y + y)+1) * 2.
 Proof.
     intro H. 
     intro x.
     eltac.rewrite H.
-    eltac.rewrite PeanoNat.Nat.mul_comm.
+    eltac.rewrite mul_comm.
     exact eq_refl.
 Defined.
 
@@ -37,8 +40,8 @@ Defined.
 Goal forall n, 2 * n = n * 2.
 Proof.
     intro n.
-    Fail eltac.rewrite PeanoNat.Nat.add_comm.
-    eltac.rewrite PeanoNat.Nat.add_comm "strong".
+    Fail eltac.rewrite add_comm.
+    eltac.rewrite add_comm "strong".
     Abort.
 
 End Example_rewrite.
diff --git a/apps/locker/tests/test_locker.v b/apps/locker/tests/test_locker.v
@@ -1,4 +1,4 @@
-From Coq Require Import ssreflect.
+From elpi.core Require Import ssreflect.
 From elpi.apps Require Import locker.
 
 (* ----------------------- *)
diff --git a/apps/tc/tests/auto_compile.v b/apps/tc/tests/auto_compile.v
@@ -2,8 +2,6 @@ From elpi.apps Require Import tc.
 
 Elpi TC Solver Override TC.Solver All.
 
-Require Import Bool.
-
 (* TODO: How to add the #[deterministic] pragma in front of the class? *)
 (* #[deterministic] Class A (T : Type) := {succ : T -> T}. *)
 Class A (T : Type) := {succ : T -> T}.
@@ -70,4 +68,4 @@ Proof.
   Import S.
   apply _.
   Fail apply _.
-Abort.
+Abort.
diff --git a/apps/tc/tests/indt_to_inst.v b/apps/tc/tests/indt_to_inst.v
@@ -1,4 +1,4 @@
-From Coq Require Export List.
+From elpi.core Require Export ListDef.
 From elpi.apps Require Export tc.
 Global Generalizable All Variables.
 
@@ -29,4 +29,4 @@ Module B.
     NoDup_elements2 (X : C) : NoDup (elements X)
   }.
 
-End B.
+End B.
diff --git a/apps/tc/tests/injTest.v b/apps/tc/tests/injTest.v
@@ -1,5 +1,5 @@
 From elpi.apps Require Import tc.
-From Coq Require Import Morphisms RelationClasses List Bool Setoid Peano Utf8.
+From elpi.core Require Import Morphisms RelationClasses ListDef Setoid.
 
 Generalizable All Variables.
 Elpi TC Solver Override TC.Solver All.
@@ -8,8 +8,8 @@ Class Inj {A B} (R : relation A) (S : relation B) (f : A -> B) :=
   inj x y : S (f x) (f y) -> R x y.
 
 Class Inj2 {A B C} (R1 : relation A) (R2 : relation B)
-    (S : relation C) (f : A → B → C) : Prop :=
-  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) → R1 x1 y1 ∧ R2 x2 y2.
+    (S : relation C) (f : A -> B -> C) : Prop :=
+  inj2 x1 x2 y1 y2 : S (f x1 x2) (f y1 y2) -> R1 x1 y1 /\ R2 x2 y2.
 
 (* Elpi TC Solver Override TC.Solver Only Inj Inj2. *)
 
@@ -65,7 +65,7 @@ Goal forall (T1 T2 : Type) (f: T1 -> T2),
 Qed. 
 
 Elpi TC Solver Override TC.Solver All.
-Local Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 ff} y : Inj R1 R3 (λ x, ff x y).
+Local Instance inj2_inj_1 `{Inj2 A B C R1 R2 R3 ff} y : Inj R1 R3 (fun x => ff x y).
 Admitted.
 
 Global Instance inj2_inj_2 `{Inj2 A B C R1 R2 R3 ff} x : Inj R2 R3 (ff x).
@@ -114,4 +114,4 @@ Proof.
   intros T x y z H.
   unfold z, y in H.
   apply _.
-Qed.
+Qed.
diff --git a/apps/tc/tests/test_pending_mode.v b/apps/tc/tests/test_pending_mode.v
@@ -1,5 +1,4 @@
 From elpi Require Import tc.
-Require Import Bool.
 
 Module m1.
   Elpi TC.Pending_mode +.
@@ -115,7 +114,7 @@ Module simplEq.
   Global Instance eqU : MyEqb unit := { eqb x y := true }.
   Global Instance eqB : MyEqb bool := { eqb x y := if x then y else negb y }.
   Global Instance eqP {A B} `{MyEqb A} `{MyEqb B} : MyEqb (A * B) := { 
-    eqb x y := (fst x == fst y) && (snd x == snd y) }.
+    eqb x y := andb (fst x == fst y) (snd x == snd y) }.
 
   Fail Goal exists T: Type, forall n m : T, eqb n m = false.
   Goal forall n m : bool, eqb n m = false. Abort.
diff --git a/examples/dune b/examples/dune
@@ -4,4 +4,12 @@
  (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.in
@@ -1042,7 +1042,8 @@ Elpi Accumulate default lp:{{
 }}.
 
 
-From Coq Require Import  Uint63.
+#[only="8.20"] From Coq Require Import Uint63.
+#[skip="8.20"] From Corelib Require Import PrimInt63.
 Open Scope uint63_scope.
 
 Fail Definition baz : list nat := default 1.  (* .fails *)
diff --git a/tests/test_API.v b/tests/test_API.v
@@ -1,5 +1,4 @@
 From elpi Require Import elpi.
-From Coq Require Vector.
 
 Elpi Command test.API.
 
diff --git a/tests/test_API2.v b/tests/test_API2.v
@@ -80,7 +80,7 @@ main [] :- !, coq.say {coq.float->float64 1.2}.
 }}.
 
 
-From Coq Require Import PrimFloat Uint63.
+From elpi.core Require Import PrimFloat PrimInt63.
 
 Open Scope uint63_scope.
 
diff --git a/tests/test_API_typecheck.v b/tests/test_API_typecheck.v
@@ -1,6 +1,6 @@
 From elpi Require Import elpi.
 
-Require Import List.
+From elpi.core Require Import ListDef.
 
 Elpi Command typecheck.
 
diff --git a/tests/test_HOAS.v b/tests/test_HOAS.v
@@ -124,11 +124,10 @@ main [trm T] :-
 }}.
 
 
-From Coq Require Import PrimInt63.
-Open Scope int63_scope.
+From elpi.core Require Import PrimInt63.
 Elpi primitive (PrimInt63.add 2000000003333002 1).
 
-From Coq Require Import PrimFloat.
+From elpi.core Require Import PrimFloat.
 Open Scope float_scope.
 Elpi primitive (2.4e13 + 1).
 End Pint.
diff --git a/tests/test_elaborator.v b/tests/test_elaborator.v
@@ -1,3 +1,5 @@
+From elpi.core Require Import PrimFloat.
+
 From elpi_elpi Extra Dependency "elpi_elaborator.elpi" as elab.
 
 From elpi Require Import elpi.
@@ -150,10 +152,8 @@ Elpi Query lp:{{get-option "of:coerce" tt =>
 }}.
 
 (* primitive *)
-From Coq Require Import Uint63.
+From elpi.core Require Import PrimInt63.
 Elpi Query lp:{{ of {{ 99%uint63 }} T X }}.
-From Coq Require Import Floats.
 Elpi Query lp:{{ of {{ 99.3e4%float }} T X }}.
-Elpi Query lp:{{ whd1 {{ (99 + 1)%uint63 }} {{ 100%uint63 }} }}.
-Elpi Query lp:{{ not(whd1 {{ (99 + _)%uint63 }} _) }}.
-
+Elpi Query lp:{{ whd1 {{ PrimInt63.add 99 1 }} {{ 100%uint63 }} }}.
+Elpi Query lp:{{ not(whd1 {{ PrimInt63.add 99 _ }} _) }}.
diff --git a/tests/test_ltac3.v b/tests/test_ltac3.v
@@ -1,6 +1,5 @@
-
 From elpi Require Export elpi.
-From Coq Require Import ssreflect ssrfun ssrbool.
+From elpi.core Require Import ssreflect ssrfun ssrbool.
 
 Ltac ltac_foo := cut True; [ idtac | abstract (exact I) ].
 
diff --git a/tests/test_synterp.v b/tests/test_synterp.v
@@ -1,4 +1,3 @@
-From Coq Require Import Bool.
 From elpi Require Import elpi.
 
 Elpi Command foo.
diff --git a/theories/attic/dune b/theories/attic/dune
@@ -0,0 +1 @@
+(include_subdirs no)
diff --git a/theories/core/Bool.v.in b/theories/core/Bool.v.in
@@ -0,0 +1,4 @@
+#[only="8.20"] From Coq Require Export Bool.
+#[only="8.20"] Module Datatypes.
+#[only="8.20"] Notation reflect := Bool.reflect.
+#[only="8.20"] End Datatypes.
diff --git a/theories/core/ListDef.v.in b/theories/core/ListDef.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export List.
+#[skip="8.20"] From Corelib Require Export ListDef.
diff --git a/theories/core/Morphisms.v.in b/theories/core/Morphisms.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export Morphisms.
+#[skip="8.20"] From Corelib Require Export Morphisms.
diff --git a/theories/core/PosDef.v.in b/theories/core/PosDef.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export PArith.
+#[skip="8.20"] From Corelib Require Export PosDef.
diff --git a/theories/core/PrimFloat.v.in b/theories/core/PrimFloat.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export Floats.
+#[skip="8.20"] From Corelib Require Export PrimFloat.
diff --git a/theories/core/PrimInt63.v.in b/theories/core/PrimInt63.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export Uint63.
+#[skip="8.20"] From Corelib Require Export PrimInt63.
diff --git a/theories/core/RelationClasses.v.in b/theories/core/RelationClasses.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export RelationClasses.
+#[skip="8.20"] From Corelib Require Export RelationClasses.
diff --git a/theories/core/Setoid.v.in b/theories/core/Setoid.v.in
@@ -0,0 +1,2 @@
+#[only="8.20"] From Coq Require Export Setoid.
+#[skip="8.20"] From Corelib Require Export Setoid.
diff --git a/theories/core/dune b/theories/core/dune
diff --git a/theories/core/ssrbool.v.in b/theories/core/ssrbool.v.in
diff --git a/theories/core/ssreflect.v.in b/theories/core/ssreflect.v.in
diff --git a/theories/core/ssrfun.v.in b/theories/core/ssrfun.v.in
diff --git a/theories/dune b/theories/dune
diff --git a/theories/wip/dune b/theories/wip/dune

Original file line number	Diff line number	Diff line change
`@@ -1,3 +1,4 @@`
	`1`	`+From elpi.core Require Import Bool.`
`1`	`2`	`From elpi.apps Require Import derive.bcongr.`
`2`	`3`
`3`	`4`	`From elpi.apps Require Import test_derive_corelib test_projK.`