The Coq mailing list

[Vladimir Voevodsky <vladimir AT ias.edu>]

Hi,

I have a type of the form (I am using a simplified example):

Definition D1 : Type := forall ( T : Type ) ( x : T ) , Type .

I now have other definitions which use D1 as a type of a parameter:

Definition DD1 ( A : D1 ) := ....

Definition DD2 ( A : D1 ) := ....

etc. 

I am going to use A : D1, mostly, fully applied i.e. in the form  A T x . I 
do not want to write T in A T x all the time since it can be easily inferred 
from x . Is there a way to write something like:

Definition D1 : Type := forall { T : Type } ( x : T ) , Type . 

and then to write A x ?

Vladimir.