The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Erik,

(In case you did not get an answer yet.)

> 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).
> ----

I don't see differences between 8.4 and 8.5 related to parsing ";".
For "( x ; y )" to factorize correctly with the parsing of parentheses
in general and of "( x , .. , y )" in particular, it has to be put at
level 0 (the underlying parser of Coq needs rules to be left manually
factorized). Do "Print Grammar constr" to evaluate the consequences of
choosing one or another parsing level. Level 0 is also to my knowledge
the level used in HoTT for "( x ; y )".

Best,

Hugo