diff options
Diffstat (limited to 'ide/ideproof.ml')
| -rw-r--r-- | ide/ideproof.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ide/ideproof.ml b/ide/ideproof.ml index 569e503c3b..12cb8c815a 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -130,6 +130,13 @@ let display mode (view:GText.view) goals hints evars = | Some { Interface.fg_goals = []; Interface.bg_goals = bg } -> (* No foreground proofs, but still unfocused ones *) view#buffer#insert "This subproof is complete, but there are still unfocused goals:\n\n"; + let rec flatten = function + | [] -> [] + | (lg, rg) :: l -> + let inner = flatten l in + List.rev_append lg inner @ rg + in + let bg = flatten (List.rev bg) in let iter goal = let msg = Printf.sprintf "%s\n" goal.Interface.goal_ccl in view#buffer#insert msg |