blob: 024243cfd359f14dfb0918788f59d98911d8956a (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
Set Implicit Arguments.
Module NonPrim.
Class foo (m : Set) := { pf : m = m }.
Notation pf' m := (pf (m := m)).
End NonPrim.
Module Prim.
Set Primitive Projections.
Class foo (m : Set) := { pf : m = m }.
Notation pf' m := (pf (m:=m)). (* Wrong argument name: m. *)
End Prim.
|
