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, 1 insertions, 0 deletions

diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 1e88456f36..1c98ec21dd 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1878,6 +1878,7 @@ let add_morphism_infer glob m n =
 	  declare_projection n instance_id (ConstRef cst)
 	| _ -> assert false
       in
+      let hook = Future.mk_hook hook in
 	Flags.silently
 	  (fun () ->
 	    Lemmas.start_proof instance_id kind (instance, ctx) hook;