From baef9828c3e6ea11fce2e172797f0f67e51885ad Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Fri, 22 May 2020 02:52:36 +0200
Subject: [nit] Remove unused exported error message in obligations

---
 vernac/obligations.mli | 1 -
 1 file changed, 1 deletion(-)

diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 102a17b216..c21951373b 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -132,5 +132,4 @@ val show_obligations : ?msg:bool -> Names.Id.t option -> unit
 val show_term : Names.Id.t option -> Pp.t
 val admit_obligations : Names.Id.t option -> unit
 
-val explain_no_obligations : Names.Id.t option -> Pp.t
 val check_program_libraries : unit -> unit
-- 
cgit v1.2.3