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