type context = hypothesis list
-type conjecture = string option * context * term
+type meta_attrs = [`Name of string | `IsSort | `InScope | `OutScope of int] list
+
+type conjecture = meta_attrs * context * term
type metasenv = (int * conjecture) list
-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 substitution = (int * subst_entry) list