| Decl of term (* type *)
| Def of term * term (* body, type *)
-type hypothesis = string * context_entry
+type hypothesis = string * context_entry (* name, entry *)
type context = hypothesis list
type metasenv = (int * conjecture) list
-type subst_entry = string option * context * term * term
+type subst_entry = string option * context * term * term (* name,ctx,bo,ty *)
type substitution = (int * subst_entry) list