aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/stm.mli
diff options
context:
space:
mode:
Diffstat (limited to 'stm/stm.mli')
-rw-r--r--stm/stm.mli3
1 files changed, 0 insertions, 3 deletions
diff --git a/stm/stm.mli b/stm/stm.mli
index 9ae78e02c..a89062c29 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -209,6 +209,3 @@ val interp : bool -> vernac_expr located -> unit
(* Queries for backward compatibility *)
val current_proof_depth : unit -> int
val get_all_proof_names : unit -> Id.t list
-
-(* Hooks to be set by other Coq components in order to break file cycles *)
-val process_error_hook : Future.fix_exn Hook.t