From 1ee892d6db3f62b7b9bbabbfde56b404bd6a8477 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thibaut=20P=C3=A9rami?= <thibaut.perami@cl.cam.ac.uk>
Date: Wed, 6 Sep 2023 12:06:06 +0200
Subject: [PATCH] Add missing Bind Scope for fin

---
 CHANGELOG.md  | 2 ++
 stdpp/fin.v   | 1 +
 tests/fin.ref | 0
 tests/fin.v   | 6 ++++++
 4 files changed, 9 insertions(+)
 create mode 100644 tests/fin.ref
 create mode 100644 tests/fin.v

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 45f87503..7c1af50c 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 5a921bbd..6ee31da6 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 00000000..e69de29b
diff --git a/tests/fin.v b/tests/fin.v
new file mode 100644
index 00000000..643d7130
--- /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.
-- 
GitLab