aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2945.v
blob: 59b57c07b704ce27d04a849f5993ffdbd941aad9 (plain)
1
2
3
4
5
Notation "f1 =1 f2 :> A" := (f1 = (f2 : A))
  (at level 70, f2 at next level, A at level 90) : fun_scope.

Notation "e :? pf" := (eq_rect _ (fun X : _ => X) e _ pf)
  (no associativity, at level 90).