Back-tracking in interactive proofs is implemented using the “timed” references of the Timed library.
Bindings in terms are implemented using the Bindlib library.
Parsing uses the Menhir library.