diff options
| -rw-r--r-- | ide/ideproof.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ide/ideproof.ml b/ide/ideproof.ml index 1e0f526a07..b79d646920 100644 --- a/ide/ideproof.ml +++ b/ide/ideproof.ml @@ -125,7 +125,7 @@ let display mode (view:GText.view) goals hints evars = in List.iter iter evs | _ -> - view#buffer#insert "Proof Completed." + view#buffer#insert "No more subgoals." end | Some { Interface.fg_goals = []; Interface.bg_goals = bg } -> (* No foreground proofs, but still unfocused ones *) |