(List.map (fun (g, _, _) -> string_of_int g)
(MatitaScript.current ())#proofMetasenv));
prerr_endline ("stack: " ^ Continuationals.Stack.pp
(List.map (fun (g, _, _) -> string_of_int g)
(MatitaScript.current ())#proofMetasenv));
prerr_endline ("stack: " ^ Continuationals.Stack.pp