1 files changed, 11 insertions, 0 deletions
diff --git a/test-suite/bugs/opened/3946.v b/test-suite/bugs/opened/3946.v
new file mode 100644
index 00000000..e77bdbc6
--- /dev/null
+++ b/test-suite/bugs/opened/3946.v
@@ -0,0 +1,11 @@
+Require Import ZArith.
+
+Inductive foo := Foo : Z.le 0 1 -> foo.
+
+Definition bar (f : foo) := let (f) := f in f.
+
+(* Doesn't work: *)
+(* Arguments bar f.*)
+
+(* Does work *)
+Arguments bar f _.