The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

I've encountered some inconvenient behavior of notation scopes.  The 
mechanism for associating notation scopes with particular parameters of 
particular definitions isn't working as I'd expect.  In particular, 
argument scope information seems to be ignored for arguments of function 
type, as I think the code below demonstrates in Coq 8.1pl3.  Is there 
something simple I could do to get the commented-out command to parse 
properly?

Inductive T : Set := t : T.

Notation "!" := t : T_scope.
Delimit Scope T_scope with T.

Definition f (_ : unit -> T) := True.
Arguments Scope f [T_scope].

Check (f (fun _ => !)%T).

(*
This fails:
Check (f (fun _ => !)).

Error message:
Toplevel input, characters 46-47
User error: Unknown interpretation for notation "!"
*)