From b209cea412a9541fd1c434dde36ea6eb1e256a33 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Thu, 16 Feb 2017 13:41:07 +0100
Subject: [stm] remove process_error_hook

`process_error_hook` seems unnecesary, we just call the proper error
interpretation.
---
 stm/stm.mli | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'stm/stm.mli')

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
-- 
cgit v1.2.3