test-suite/bugs/opened/3946.v


1
2
3
4
5
6
7
8
9
10
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 _.