Add missing Bind Scope for fin

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

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

tests/fin.v

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