The Coq mailing list

["Carlos.SIMPSON" <carlos AT math.unice.fr>]

Regarding Judicael Courant's message---
would it be possible to support A. Miquel' suggestion?

This solution (if it exists) would seem to reply fairly well to 
(2) and (3) and if the user is well-informed, to (1) too.

One would have to
respond to what Miquel called ``all the problems ''
(he said ``this doesnt fix all the problems ...'')?

I don't know what these all are but I did find one when I tried
to implement his suggestion: you couldn't type
Record foo : Type3 := {
etc 
}

for example, because Type3 isn't a  sortdef. 
Would it be possible to make the system accept T as a sortdef whenever
 T := Type is declared?

This seems to create a limited possibility for ``subtypes'' since
in effect Type1 becomes a subtype of Type2 and so on. 
Do these subtypes (or subsorts) cause some problem? 

When I tried implementing Miquel's suggestion something went wrong, 
cf the big file that I sent to 
coq@...
 a while ago;
but I don't know what it was. It may just have been due to our old 
version of coq or maybe a stupid mistake on my part.

---Carlos