(* Max of non-empty list of named universes, or their successor (when true)
* The empty list represents type0 *)
type sort = Prop | Type of universe
(* Max of non-empty list of named universes, or their successor (when true)
* The empty list represents type0 *)
type sort = Prop | Type of universe
-type subst_entry = string option * context * term * term (* name,ctx,bo,ty *)
+type subst_entry = meta_attrs * context * term * term (* name,ctx,bo,ty *)
type i_attr = generated * ind_pragma
(* invariant: metasenv and substitution have disjoint domains *)
type i_attr = generated * ind_pragma
(* invariant: metasenv and substitution have disjoint domains *)