blob: e77bdbc652ae295af9b44c7420808331281064ae (
plain)
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 _.
|