If there are no focused goals, print the unfocused goals

Match the coqide's goal message format. This is important for indicating
whether an unfocused goal needs to be focused or the proof is done.

autoload/coquille.py

@@ -303,10 +303,22 @@ def show_goal(self, feedback_callback):
             goals = response.val.val
 
             sub_goals = goals.fg
+            msg_format = '{0} subgoal{1}'
+            if not sub_goals:
+                sub_goals = []
+                for (before, after) in goals.bg:
+                    sub_goals.extend(reversed(before))
+                    sub_goals.extend(after)
+                if sub_goals:
+                    msg_format = ('This subproof is complete, but there {2} {0}'
+                                  ' unfocused goal{1}')
+            if not sub_goals:
+                msg_format = 'No more subgoals.'
 
             nb_subgoals = len(sub_goals)
-            plural_opt = '' if nb_subgoals == 1 else 's'
-            self.goal_buffer[0] = '%d subgoal%s' % (nb_subgoals, plural_opt)
+            self.goal_buffer[0] = msg_format.format(nb_subgoals,
+                                                    '' if nb_subgoals == 1 else 's',
+                                                    'is' if nb_subgoals == 1 else 'are')
             self.goal_buffer.append([''])
 
             for idx, sub_goal in enumerate(sub_goals):