From e262a6262ebb6c3010cb58e96839b0e3d66e09ac Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 11 Apr 2020 17:19:12 -0400
Subject: [proof] Move functions related to `Proof.t` to `Proof`

This makes the API more orthogonal and allows better structure in
future code.
---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

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.")
 
-- 
cgit v1.2.3