From e18c553a4ab27ecabebd968fe4f2fdd18ea19101 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 00:49:56 +0100
Subject: [vernacular] Make `Show` fail again when no goals remain.

This is used in the test-suite to check that a proof is closed; I am
not sure we'd like to keep this patch tho: the non-failing semantics
seems saner for IDEs.

[main users are in `test-suite/ide`]
---
 vernac/vernacentries.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 284df19b4c..e6a5f5e7b4 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -105,7 +105,8 @@ let show_proof ~pstate =
   (* We print nothing if there are no goals left *)
   with
   | Pfedit.NoSuchGoal
-  | Option.IsNone -> mt ()
+  | Option.IsNone ->
+    user_err (str "No goals to show.")
 
 let show_top_evars ~pstate =
   (* spiwack: new as of Feb. 2010: shows goal evars in addition to non-goal evars. *)
@@ -2116,7 +2117,8 @@ let vernac_show ~pstate =
       | ShowProof -> show_proof ~pstate
       | ShowMatch id -> show_match id
       | ShowScript -> assert false  (* Only the stm knows the script *)
-      | _ -> mt ()
+      | _ ->
+        user_err (str "This command requires an open proof.")
     end
   (* Show functions that require a proof state *)
   | Some pstate ->
-- 
cgit v1.2.3