1 files changed, 12 insertions, 14 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 3934a29413..606cfade46 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Decl_kinds
 
 type locality = Discharge | Global of Declare.import_status
 
@@ -22,29 +21,28 @@ module Hook : sig
      as a Coercion, perform some cleanup, update the search database,
      etc...  *)
   module S : sig
-    (** [S.t] passes to the client: *)
-    type t
-      =  UState.t
+    type t =
+      { uctx : UState.t
       (** [ustate]: universe constraints obtained when the term was closed *)
-      -> (Id.t * Constr.t) list
+      ; obls : (Id.t * Constr.t) list
       (** [(n1,t1),...(nm,tm)]: association list between obligation
           name and the corresponding defined term (might be a constant,
           but also an arbitrary term in the Expand case of obligations) *)
-      -> locality
-      (**  [locality]: Locality of the original declaration *)
-      -> GlobRef.t
-      (** [ref]: identifier of the original declaration *)
-      -> unit
+      ; scope : locality
+      (** [scope]: Locality of the original declaration *)
+      ; dref : GlobRef.t
+      (** [dref]: identifier of the original declaration *)
+      }
   end
 
-  val make : S.t -> t
-  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t
+  val make : (S.t -> unit) -> t
+  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit
 end
 
 val declare_definition
   :  name:Id.t
   -> scope:locality
-  -> kind:definition_object_kind
+  -> kind:Decls.definition_object_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> UnivNames.universe_binders
   -> Evd.side_effects Proof_global.proof_entry
@@ -56,7 +54,7 @@ val declare_fix
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> name:Id.t
   -> scope:locality
-  -> kind:definition_object_kind
+  -> kind:Decls.definition_object_kind
   -> UnivNames.universe_binders
   -> Entries.universes_entry
   -> Evd.side_effects Entries.proof_output