Adapt to coq/coq#19530

proux01 · Sep 19, 2024 · 5f0ec45 · 5f0ec45
1 parent 9c8a9da
commit 5f0ec45
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 5 deletions.
diff --git a/examples/RedBlack/dune b/examples/RedBlack/dune
@@ -6,3 +6,8 @@
     testing
     verif
   ))
+
+(rule
+  (alias testing)
+  (target testing.v)
+  (action (run sh %{dep:../../scripts/mycppo} %{dep:testing.v.cppo} %{target})))
diff --git a/examples/RedBlack/testing.v → examples/RedBlack/testing.v.cppo b/examples/RedBlack/testing.v → examples/RedBlack/testing.v.cppo
@@ -158,7 +158,11 @@ Proof.
   apply wf_lexprod. now apply Wf_nat.lt_wf. intros _; now apply well_foulded_ltColor.
 Qed.
 
-Require Import Program.Wf. Import WfExtensionality.
+#if COQ_VERSION >= (8, 21, 0)
+From Stdlib.Program Require Import Wf WfExtensionality. Import WfExtensionality.
+#else
+From Coq.Program Require Import Wf. Import WfExtensionality.
+#endif
 Require Import FunctionalExtensionality.
 
 (* begin genRBTree_height *)

diff --git a/examples/other/enumProofs.v b/examples/other/enumProofs.v
@@ -2,7 +2,7 @@ From QuickChick Require Import QuickChick Tactics TacticsUtil Instances
      Classes DependentClasses Sets EnumProofs.
 
 Require Import String. Open Scope string.
-Require Import List micromega.Lia.
+From Coq Require Import List Lia.
 
 
 From Ltac2 Require Import Ltac2.

diff --git a/src/Classes.v b/src/Classes.v
@@ -1,4 +1,4 @@
-From Coq Require Import List Morphisms Recdef ZArith ZArith.Znat Arith.
+From Coq Require Import List Morphisms Recdef ZArith Znat Arith.
 From QuickChick  Require Import Sets Tactics Producer Generators Enumerators.
 
 Set Bullet Behavior "Strict Subproofs".

diff --git a/src/LazyList.v b/src/LazyList.v
@@ -344,7 +344,7 @@ Fixpoint filter_LazyList {A} (p : A -> bool) (l : LazyList A) :=
                  else filter_LazyList p (t tt)
   end.
 
-Require Import Coq.Logic.ClassicalFacts.
+From Coq.Logic Require Import ClassicalFacts.
 
 Axiom EM : excluded_middle.
 

diff --git a/src/TacticsUtil.v.cppo b/src/TacticsUtil.v.cppo
@@ -27,7 +27,7 @@ Ltac2 Notation "inv" h(ident) := inv_tac h.
 Local Ltac2 exfalso_tac () := ltac1:(exfalso).
 Ltac2 Notation "exfalso" := exfalso_tac ().
 
-Local Ltac2 lia_ltac1 () := ltac1:(micromega.Lia.lia).
+Local Ltac2 lia_ltac1 () := ltac1:(Lia.lia).
 Ltac2 Notation "lia" := lia_ltac1 ().
 
 Ltac2 inv := fun (h : ident) =>  inversion h; subst.