diff --git a/CHANGELOG.md b/CHANGELOG.md
index 45f875030940f04809f9f7f013851aab5f1817e9..7c1af50c5ea2cc146662ac91ccfdfeda51894b69 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -69,6 +69,8 @@ longer supported by this release.
   `Fixpoint f (t : gtest) := let 'GTest ts := t in map_fold (λ _ t', plus (f t')) 1 ts`.
 - Make `fin` number literal notations work with numbers above 10. (by Thibaut
   Pérami)
+- Bind `fin` type to `fin` scope, so function taking a `fin` as argument will
+  implicitly parse it in `fin` scope (by Thibaut Pérami).
 - Change premise `Equivalence` into `PreOrder` for `set_fold_proper`.
 - Weaken `Proper` premises of `set_ind`, `set_fold_ind`, `set_fold_proper`. If
   you use `solve_proper` to solve these premises, no change should be needed. If
diff --git a/stdpp/fin.v b/stdpp/fin.v
index 5a921bbdc162f7a3a7cedb006f86d19844f66ac1..6ee31da6ab1573cd0d116e059a69c07e0cae3eb3 100644
--- a/stdpp/fin.v
+++ b/stdpp/fin.v
@@ -17,6 +17,7 @@ Notation FS := Fin.FS.
 
 Declare Scope fin_scope.
 Delimit Scope fin_scope with fin.
+Bind Scope fin_scope with fin.
 Global Arguments Fin.FS _ _%fin : assert.
 
 (** Allow any non-negative number literal to be parsed as a [fin]. For example
diff --git a/tests/fin.ref b/tests/fin.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/fin.v b/tests/fin.v
new file mode 100644
index 0000000000000000000000000000000000000000..643d71308646c1a68fea052d744cc3ea7d563318
--- /dev/null
+++ b/tests/fin.v
@@ -0,0 +1,6 @@
+From stdpp Require Import fin.
+
+Definition f n m (p : fin n) := m < p.
+
+Lemma test : f 47 13 32.
+Proof. vm_compute. lia. Qed.