Adapt to rocq-prover/rocq#19530

Author: proux01

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})))

examples/RedBlack/testing.v renamed to 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 *)

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.

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".

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.
 

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.