The Coq mailing list

[anoun AT labri.fr]

Hi,
In Coq's kernel, we find two data types which are constr and kind of term,
what's the difference between them??
If we have a constr c, we can obtain it's kind of term using (kind_of_term c),
can we do the opposite? i.e. build a constr using a kind-of-term??
Thanks a lot
Houda

----------------------------------------------------------------
This message was sent using IMP, the Internet Messaging Program.