+
+type object_class =
+ [ `Coercion
+ | `Elim of sort (** elimination principle; if sort is Type, the universe is
+ * not relevant *)
+ | `Record of string list (** inductive type that encodes a record;
+ the arguments are the record fields *)
+ | `Projection (** record projection *)
+ ]
+
+type attribute =
+ [ `Class of object_class
+ | `Generated
+ ]
+
+type term =
+ Rel of int (* DeBrujin index, 1 based*)