| Appl of term * term (* application: argument, function *)
| Abst of id * term * term (* abstraction: name, domain, scope *)
-type entity = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *)
- | Context of qid option (* context: Some = last node, None = root *)
- | Block of id * term (* block opener: name, domain *)
- | Decl of id * term (* declaration: name, domain *)
- | Def of id * term * bool * term (* definition: name, domain, transparent?, body *)
+type command = Section of (bool * id) option (* section: Some true = open, Some false = reopen, None = close last *)
+ | Context of qid option (* context: Some = last node, None = root *)
+ | Block of id * term (* block opener: name, domain *)
+ | Decl of id * term (* declaration: name, domain *)
+ | Def of id * term * bool * term (* definition: name, domain, transparent?, body *)