adapt to rocq-prover/stdlib#154

Author: mrhaandi

theories/FOL/Sets/Models/HF_model.v

@@ -494,7 +494,7 @@ Qed.
 Lemma list_numerals_nodup n :
   NoDup (list_numerals n).
 Proof.
-  apply FinFun.Injective_map_NoDup.
+  apply Finite.Injective_map_NoDup.
   - intros k k'. apply hfs_numeral_inj.
   - apply list_n_nodup.
 Qed.

theories/HOU/calculus/equivalence.v

@@ -1,5 +1,5 @@
 Set Implicit Arguments.
-From Stdlib Require Import Morphisms Lia FinFun.
+From Stdlib Require Import Morphisms Lia Finite.
 From Undecidability.HOU Require Import std.std.
 From Undecidability.HOU.calculus Require Import 
   prelim terms syntax semantics confluence. 

theories/HOU/calculus/semantics.v

@@ -1,6 +1,6 @@
 Set Implicit Arguments.
 From Undecidability.HOU Require Import calculus.prelim calculus.terms calculus.syntax std.std.
-From Stdlib Require Import Morphisms Lia FinFun. 
+From Stdlib Require Import Morphisms Lia Finite. 
 
 (* * Semantics **)
 Section Semantics.

theories/HOU/calculus/terms_extension.v

@@ -1,5 +1,5 @@
 Set Implicit Arguments.
-From Stdlib Require Import List Arith Lia Morphisms FinFun.
+From Stdlib Require Import List Arith Lia Morphisms Finite.
 Import ListNotations.
 From Undecidability.HOU Require Import std.std.
 From Undecidability.HOU.calculus Require Import 

theories/HOU/second_order/goldfarb/multiplication.v

@@ -3,7 +3,7 @@ From Stdlib Require Import List Lia Program.Program.
 From Undecidability.HOU Require Import std.std axioms.
 From Stdlib Require Import RelationClasses Morphisms Init.Wf Init.Nat Setoid.
 From Undecidability.HOU Require Import calculus.calculus second_order.goldfarb.encoding.
-From Stdlib Require Import FinFun Arith.Wf_nat.
+From Stdlib Require Import Finite Arith.Wf_nat.
 Import ListNotations ArsInstances.
 
 

theories/HOU/std/ars/basic.v

@@ -4,7 +4,7 @@ http://www.ps.uni-saarland.de/courses/sem-ws17/confluence.v
  *)
 
 Set Implicit Arguments.
-From Stdlib Require Import Morphisms FinFun.
+From Stdlib Require Import Morphisms Finite.
 From Undecidability.HOU Require Import std.tactics.
 
 Section ClosureRelations.

theories/HOU/std/ars/confluence.v

@@ -4,7 +4,7 @@ http://www.ps.uni-saarland.de/courses/sem-ws17/confluence.v
  *)
 
 Set Implicit Arguments.
-From Stdlib Require Import Morphisms FinFun.
+From Stdlib Require Import Morphisms Finite.
 From Undecidability.HOU Require Import std.tactics std.misc std.ars.basic.
 Import ArsInstances.
 #[export] Hint Constructors star : core.

theories/HOU/std/ars/evaluator.v

@@ -4,7 +4,7 @@ http://www.ps.uni-saarland.de/courses/sem-ws17/confluence.v
  *)
 
 Set Implicit Arguments.
-From Stdlib Require Import Morphisms FinFun ConstructiveEpsilon.
+From Stdlib Require Import Morphisms Finite ConstructiveEpsilon.
 From Undecidability.HOU Require Import std.tactics std.decidable std.misc std.ars.basic std.ars.confluence.
 Import ArsInstances.
 Section Evaluator.

theories/HOU/std/ars/list_reduction.v

@@ -1,5 +1,5 @@
 Set Implicit Arguments.
-From Stdlib Require Import List Morphisms FinFun.
+From Stdlib Require Import List Morphisms Finite.
 From Undecidability.HOU Require Import std.tactics std.ars.basic std.ars.confluence.
 Import ListNotations ArsInstances.
 Section ListRelations.

theories/HOU/std/countability.v

@@ -1,5 +1,5 @@
-Set Implicit Arguments. 
-From Stdlib Require Import FinFun.
+Set Implicit Arguments.
+From Stdlib Require Import Finite.
 From Undecidability.HOU Require Import std.decidable.
 
 Inductive diag: nat -> nat -> Type :=