method proofContext =
match userGoal with
- None -> assert false
- | Some n ->
- GrafiteTypes.get_proof_context self#grafite_status n
+ None -> []
+ | Some n -> GrafiteTypes.get_proof_context self#grafite_status n
method proofConclusion =
match userGoal with