diff options
| -rw-r--r-- | stm/stm.mli | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/stm/stm.mli b/stm/stm.mli index 9cf5206cfa..a0bbe05b3a 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -288,8 +288,10 @@ val forward_feedback_hook : (Feedback.feedback -> unit) Hook.t (** User adds a sentence to the document (after parsing) *) val document_add_hook : (Vernacexpr.vernac_control -> Stateid.t -> unit) Hook.t + (** User edits a sentence in the document *) val document_edit_hook : (Stateid.t -> unit) Hook.t + (** User requests evaluation of a sentence *) val sentence_exec_hook : (Stateid.t -> unit) Hook.t |