-and lenv = ESort (* top *)
- | EBind of lenv * attrs * bind (* environment, attrs, binder *)
- | EAppl of lenv * attrs * bool * term (* environment, attrs, extended?, argument *)
- | EProj of lenv * attrs * lenv (* environment, attrs, closure *)
+and term = TSort of int (* hierarchy index *)
+ | TLRef of n_attrs * int (* attrs, position indexe *)
+ | TGRef of n_attrs * uri (* attrs, reference *)
+ | TCast of term * term (* domain, element *)
+ | TAppl of a_attrs * term * term (* attrs, argument, function *)
+ | TBind of b_attrs * bind * term (* attrs, binder, scope *)
+ | TProj of lenv * term (* closure, member *)
+
+and lenv = ESort (* top *)
+ | EBind of lenv * n_attrs * b_attrs * bind (* environment, attrs, binder *)
+ | EAppl of lenv * a_attrs * term (* environment, attrs, argument *)
+ | EProj of lenv * lenv (* environment, closure *)