-type item = Section of id option (* section: Some = open/reopen, None = close last *)
- | Context of qid option (* context: Some = last node, None = root *)
- | Block of id * term (* block opener: name, type *)
- | Decl of id * term (* declaration: name, type *)
- | Def of id * term * bool * term (* definition: name, type, 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 *)