diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 37808a3726..860671aed7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -100,7 +100,7 @@ let show_proof ~pstate = Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf (* We print nothing if there are no goals left *) with - | Declare.NoSuchGoal + | Proof.NoSuchGoal _ | Option.IsNone -> user_err (str "No goals to show.") |