-type entity = Section of id option (* section: Some id = open, None = close last *)
- | Global of bool * id * comm * term (* global entity: false = decl, true = def *)
+and term = Sort of ix (* level *)
+ | NSrt of id (* named level *)
+ | LRef of ix * ix (* index, offset *)
+ | NRef of id (* name *)
+ | Cast of term * term (* domain, element *)
+ | Appl of term list * term (* arguments, function *)
+ | Bind of bind * term (* binder, scope *)
+ | Inst of term * term list (* function, arguments *)
+ | Impl of bool * id * term * term (* strong?, label, source, target *)
+
+type command = Require of id list (* required files: names *)
+ | Graph of id (* hierarchy graph: name *)
+ | Sorts of (int option * id) list (* sorts: index, name *)
+ | Section of id option (* section: Some id = open, None = close last *)
+ | Entity of kind * id * desc * term (* entity: class, name, description, contents *)
+ | Generate of term list (* predefined generated entity: arguments *)
+