aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/3624.v
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.