The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Sunday, October 13, 2013, Enrico Tassi  wrote:
> But I've a more general remark.  I do swich Coq versions too, but
>
> I don't think I qualify as a regular user.  IMO users should stick to
> the stable version, unless they want to develop Coq or a plugin.

The homotopy type theorists require a version of Coq which supports universe polymorphism, some sort of higher inductive types, and a different universe numbering scheme which doesn't permit one to smuggle isomorphisms into [Prop], even with univalence.

I tend to switch between two versions regularly (v8.4pl2, and HoTT/coq), though I also sometimes use Bruno's version of Coq to play with nicer higher inductive types, and Matthieu's version of Coq to play with eta for records.