Module Proofview_monad.Trace

type 'a forest = 'a tree list

The intent is that an 'a forest is a list of messages of type 'a. But messages can stand for a list of more precise messages, hence the structure is organised as a tree.

and 'a tree =
| Seq of 'a * 'a forest
type 'a incr

To build a trace incrementally, we use an intermediary data structure on which we can define an S-expression like language (like a simplified xml except the closing tags do not carry a name).

val to_tree : 'a incr -> 'a forest
val opn : 'a -> 'a incr -> 'a incr

open a opens a tag with name a.

val close : 'a incr -> 'a incr

close closes the last open tag. It is the responsibility of the user to close all the tags.

val leaf : 'a -> 'a incr -> 'a incr

leaf creates an empty tag with name a.