diff options
| author | Emilio Jesus Gallego Arias | 2019-02-12 00:49:56 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-03-27 23:56:18 +0100 |
| commit | e18c553a4ab27ecabebd968fe4f2fdd18ea19101 (patch) | |
| tree | d2045ba4963a8c7e02817eb95dee35b579a0f664 | |
| parent | 43f3634a0e75381ca473aea08415e3d262e4c066 (diff) | |
[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`]
| -rw-r--r-- | vernac/vernacentries.ml | 6 |
1 files 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 -> |