Enforce a correct exception handling in declaration_hooks

This should finally get rid of the following class of bugs:
Qed fails, STM undoes to the beginning of the proof because the
exception is not annotated with the correct state, PG gets out of
sync because errors always refer to the last command in PGIP.

1 files changed, 7 insertions, 0 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 77386a1a9..960363e25 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -91,6 +91,13 @@ let from_val ?(fix_exn=id) v = create fix_exn (Val (v, None))
 let from_here ?(fix_exn=id) v = create fix_exn (Val (v, Some (!freeze ())))
 
 let fix_exn_of ck = let _, fix_exn, _ = get ck in fix_exn
+type 'a hook = Decl_kinds.locality -> Globnames.global_reference -> 'a
+let mk_hook hook = hook
+let call_hook fix_exn hook l c =
+  try hook l c
+  with e when Errors.noncritical e ->
+    let e = Errors.push e in
+    raise (fix_exn e)
 
 let default_force () = raise NotReady
 let assignement ck = fun v ->