type context = hypothesis list
-type conjecture = string option * context * term
+type meta_attr =
+ [ `Name of string
+ | `IsTerm | `IsType | `IsSort
+ | `InScope | `OutScope of int]
+
+type meta_attrs = meta_attr 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