[proof] Miscellaneous cleanup on proof info handling

After the refactorings proof information is organized in a slightly
different way thus the lower layers don't need to pass info back
anymore.

1 files changed, 1 insertions, 1 deletions

diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1d7fd3a3bf..e999027b44 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -36,7 +36,7 @@ module Hook : sig
   end
 
   val make : (S.t -> unit) -> t
-  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit
+  val call : ?hook:t -> S.t -> unit
 end
 
 val declare_definition