[declare] Generalize type of hooks.

This is essential to allow hooks to modify state.

2 files changed, 9 insertions, 4 deletions

diff --git a/vernac/declare.ml b/vernac/declare.ml
index 85359d5b62..a7da245b0f 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -33,11 +33,13 @@ module Hook = struct
       }
   end
 
-  type t = (S.t -> unit) CEphemeron.key
+  type 'a g = (S.t -> 'a -> 'a) CEphemeron.key
+  type t = unit g
 
-  let make hook = CEphemeron.create hook
+  let make_g hook = CEphemeron.create hook
+  let make (hook : S.t -> unit) : t = CEphemeron.create (fun x () -> hook x)
 
-  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x ()) hook
 
 end
 
diff --git a/vernac/declare.mli b/vernac/declare.mli
index 4891e66803..e13611a828 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -40,7 +40,9 @@ open Names
    care, as imperative effects may become not supported in the
    future. *)
 module Hook : sig
-  type t
+  type 'a g
+
+  type t = unit g
 
   (** Hooks allow users of the API to perform arbitrary actions at
      proof/definition saving time. For example, to register a constant
@@ -61,6 +63,7 @@ module Hook : sig
       }
   end
 
+  val make_g : (S.t -> 'a -> 'a) -> 'a g
   val make : (S.t -> unit) -> t
   val call : ?hook:t -> S.t -> unit
 end