(** list of states before having executed statements. Head element of this
* list is the current state, last element is the state at the beginning of
* the script.
(** list of states before having executed statements. Head element of this
* list is the current state, last element is the state at the beginning of
* the script.