+type context_entry = (* A declaration or definition *)
+ | Decl of term
+ | Def of term * term option (* body, type (if known) *)
+
+type hypothesis = string * context_entry (* None means no more accessible *)
+
+type context = hypothesis list
+
+type conjecture = int * string option * context * term
+
+type metasenv = conjecture list
+
+type substitution = (int * (string option * context * term * term)) list
+
+
+
+
+type inductiveFun =
+ string * int * term * term (* if coinductive, the int has no meaning and must be set to -1 *)
+
+type constructor = string * term (* id, type *)
+
+type inductiveType =
+ string * bool * term * (* typename, inductive, arity *)
+ constructor list (* constructors *)
+
+type def_flavour = (* presentational *)
+ [ `Definition
+ | `Fact
+ | `Lemma
+ | `Remark
+ | `Theorem
+ ]
+
+type def_pragma = (* pragmatic of the object *)
+ [ `Coercion of int
+ | `Elim of sort (** elimination principle; if sort is Type, the universe is not relevant *)
+ | `Projection (** record projection *)
+ | `InversionPrinciple (** inversion principle *)
+ | `Variant
+ ]
+
+type ind_pragma = (* pragmatic of the object *)
+ [ `Record of (string * bool * int) list (**
+ inductive type that encodes a record; the arguments are
+ the record fields names and if they are coercions and
+ then the coercion arity *)
+ ]
+
+type generated = [ `Generated | `Provided ]
+
+type c_attr = generated * def_flavour * def_pragma
+type f_attr = generated * def_flavour
+type i_attr = generated * ind_pragma
+
+type obj =
+ | Constant of NUri.uri * metasenv * substitution * string * term option * term * c_attr
+ | Fixpoint of NUri.uri * metasenv * substitution * bool * inductiveFun list * f_attr
+ | Inductive of NUri.uri * metasenv * substitution * inductiveType list * i_attr