| Appl of term * term (* application: argument, function *)
| Abst of id * term * term (* abstraction: name, type, body *)
-type item = Section of id option (* section: Some = open/reopen, None = close last *)
+type item = 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, type *)
| Decl of id * term (* declaration: name, type *)