The Coq mailing list

[Erik Palmgren <palmgren AT math.su.se>]

I am porting a rather large development from Hcoq/HoTT to Coq 8.5beta 
and try to regain the old dot (.1, .2) and pairing notation ( ; ) for 
existT as below. However this seems to interfere with other notation 
(either records or sigT). Is ( ; ) dealt with in some special way in 8.4?

----
Notation "x .1" := (projT1 x) (at level 0).
Notation "x .2" := (projT2 x) (at level 0).
Notation "( x ; y )" := (existT _ x y) (at level 99).
----

Grateful for any hints.

Erik Palmgren