From b49c80406f518d273056b2143f55e23deeea2813 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 30 Oct 2015 18:15:58 +0100 Subject: Command.declare_definition: grab the fix_exn early (follows 77cf18e) When a future is fully forced (joined), the fix_exn is dropped, since joined futures are values (hence they cannot raise exceptions). When a future for a transparent definition enters the environment it is joined. If one needs to pick its fix_exn, he should do it before that. --- toplevel/command.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/toplevel/command.ml b/toplevel/command.ml index 73fd3d1a4..3d338ee0a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -154,6 +154,7 @@ let set_declare_definition_hook = (:=) declare_definition_hook let get_declare_definition_hook () = !declare_definition_hook let declare_definition ident (local, p, k) ce pl imps hook = + let fix_exn = Future.fix_exn_of ce.const_entry_body in let () = !declare_definition_hook ce in let r = match local with | Discharge when Lib.sections_are_opened () -> @@ -170,7 +171,7 @@ let declare_definition ident (local, p, k) ce pl imps hook = gr | Discharge | Local | Global -> declare_global_definition ident ce local k pl imps in - Lemmas.call_hook (Future.fix_exn_of ce.const_entry_body) hook local r + Lemmas.call_hook fix_exn hook local r let _ = Obligations.declare_definition_ref := (fun i k c imps hook -> declare_definition i k c [] imps hook) -- cgit v1.2.3