- | Type
-and name =
- Name of string
- | Anonimous
-and term =
- Rel of int (* DeBrujin index *)
- | Var of UriManager.uri (* uri *)
- | Meta of int (* numeric id *)
+ | Type of CicUniv.universe
+ | CProp
+
+type name =
+ | Name of string
+ | Anonymous
+
+type object_flavour =
+ [ `Definition
+ | `Fact
+ | `Lemma
+ | `Remark
+ | `Theorem
+ | `Variant
+ ]
+
+type object_class =
+ [ `Coercion
+ | `Elim of sort (** elimination principle; if sort is Type, the universe is
+ * not relevant *)
+ | `Record of (string * bool) list (**
+ inductive type that encodes a record; the arguments are
+ the record fields names and if they are coercions *)
+ | `Projection (** record projection *)
+ ]
+
+type attribute =
+ [ `Class of object_class
+ | `Flavour of object_flavour
+ | `Generated
+ ]
+
+type term =
+ Rel of int (* DeBrujin index, 1 based*)
+ | Var of UriManager.uri * (* uri, *)
+ term explicit_named_substitution (* explicit named subst. *)
+ | Meta of int * (term option) list (* numeric id, *)
+ (* local context *)