type context = hypothesis list
-type meta_attrs = [`Name of string | `IsSort | `InScope | `OutScope of int] list
+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