+ let first = ref true in
+ let res = ref [] in
+ let push_res () =
+ res :=
+ { term = Buffer.contents term;
+ emetasenv = Buffer.contents emetasenv;
+ eterm = Buffer.contents eterm;
+ etype = Buffer.contents etype;
+ ereduced = Buffer.contents ereduced } :: !res ;
+ in
+ Buffer.clear term;