Import FInFun (#825)

andrew-appel · andres-erbsen · web-flow · commit 644b83079487 · 2025-07-01T10:17:00.000-04:00
* use RelationClasses instead of old Relations_1 (for rocq-prover/stdlib#152) * 'make test2' now builds in Rocq 9 with dev versions of Flocq and CompCert --------- Co-authored-by: Andres Erbsen <andres@andres.systems>
diff --git a/InteractionTrees b/InteractionTrees
@@ -1 +1 @@
-Subproject commit e7fed212b1061b358428b57e11ee489184e241a2
+Subproject commit cf1443c88aca8691d93ce84fc633145752e7944e
diff --git a/coq-ext-lib b/coq-ext-lib
@@ -1 +1 @@
-Subproject commit 4811a83db9ccd81f4dcbf77eeff0484dfb21a48b
+Subproject commit b27e806daf39a8f1cfc7ced09c1af44d390af4a6
diff --git a/fcf b/fcf
@@ -1 +1 @@
-Subproject commit d0f5432b902f452dcb2c85dc1981243dd4963977
+Subproject commit 866d37a03eee51dd9c541ffa9449094af2b09309
diff --git a/msl/subtypes.v b/msl/subtypes.v
@@ -3,12 +3,11 @@
  *
  *)
 
+Require Import Arith.
 Require Import VST.msl.base.
 Require Import VST.msl.ageable.
 Require Import VST.msl.predicates_hered.
 
-Import Arith.
-
 Local Open Scope pred.
 
 Section Fash.
diff --git a/paco b/paco
@@ -1 +1 @@
-Subproject commit 5c5693f46c8957f36a2349a0d906e911366136de
+Subproject commit d0561bf7f0a96cac486ba3bd8ca0b72ce01fb9cf
diff --git a/progs64/io_os_connection.v b/progs64/io_os_connection.v
@@ -565,11 +565,13 @@ Section Invariants.
     intros Hin; apply in_combine_l in Hin; easy.
   Qed.
 
+Require Import FinFun.
+
   Lemma mkRecvEvents_NoDup : forall logIdx cs,
     NoDup (mkRecvEvents logIdx cs).
   Proof.
     unfold mkRecvEvents, enumerate; intros.
-    apply FinFun.Injective_map_NoDup; auto using combine_NoDup, seq_NoDup.
+    apply Injective_map_NoDup; auto using combine_NoDup, seq_NoDup.
     red; intros (? & ?) (? & ?); intros; inj; auto.
   Qed.
 
diff --git a/zlist/list_solver.v b/zlist/list_solver.v
@@ -1,3 +1,4 @@
+Require Import RelationClasses.
 Require Import ZArith Znumtheory.
 Require Import Coq.Lists.List.
 Require Import Lia.
@@ -1030,8 +1031,8 @@ Section Sorted.
 Variable A : Type.
 Variable d : Inhabitant A.
 Variable le : A -> A -> Prop.
-Context {Hrefl : Relations_1.Reflexive A le}.
-Context {Htrans : Relations_1.Transitive le}.
+Context {Hrefl : Reflexive le}.
+Context {Htrans : Transitive le}.
 
 Definition sorted (l : list A) :=
   forall i j, 0 <= i <= j /\ j < Zlength l -> le (Znth i l) (Znth j l).
