blob: a05d5eb21527d0080de7c2b196c970b2762e3a85 (
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.
|
