+ let get_stack (status, _) = GT.get_stack status
+
+ let get_status (status, goal) =
+ match status.GT.proof_status with
+ | GT.Incomplete_proof incomplete -> incomplete.GT.proof, goal
+ | _ -> assert false
+
+ let get_proof (status, _, _) =
+ match status.GT.proof_status with
+ | GT.Incomplete_proof incomplete -> incomplete.GT.proof
+ | _ -> assert false