The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Sun, Oct 13, 2013 at 10:12:47AM -0400, Jason Gross wrote:
> > I do swich Coq versions too, but
> > I don't think I qualify as a regular user.
> 
> 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.

Maybe my definition of regular user is a bit too strict, and cuts out
some legitimate research activity.

Still you are jumping between experimental implementations of unfinished
type theories that happen to be based on Coq.  To my eyes, you too do
not qualify as a regular Coq user.

Cheers
-- 
Enrico Tassi