Rocq 9.0 compatibility

nchappe · nchappe · commit b9fd304c5fbd · 2025-07-17T15:24:23.000+02:00
diff --git a/examples/Yield/Par.v b/examples/Yield/Par.v
@@ -1,9 +1,9 @@
 From Coq Require Import
      Program
      List
-     Logic.FinFun
      Logic.FunctionalExtensionality
      Logic.IndefiniteDescription
+     Vectors.FinFun
      micromega.Lia
      Init.Specif
      Fin.
diff --git a/examples/Yield/Util.v b/examples/Yield/Util.v
@@ -1,9 +1,9 @@
 From Coq Require Import
      Program
      List
-     Logic.FinFun
      Logic.FunctionalExtensionality
      Logic.IndefiniteDescription
+     Vectors.FinFun
      micromega.Lia
      Init.Specif
      Fin.
diff --git a/tests/ImpBrTest/extracted/dune b/tests/ImpBrTest/extracted/dune
@@ -12,7 +12,6 @@
     Basics
     BinNat
     BinNums
-    BinPosDef
     BinPos
     Bool
     Byte
@@ -39,6 +38,7 @@
     Interp
     ITreeDefinition
     List0
+    ListDef
     Logic
     MapDefault
     Maps
@@ -56,6 +56,7 @@
     Number
     OptionMonad
     PeanoNat
+    PosDef
     ReaderMonad
     Reducible
     RelDec
