aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--vernac/obligations.mli1
1 files changed, 0 insertions, 1 deletions
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