diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-30 18:15:58 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-10-30 18:15:58 +0100 |
| commit | b49c80406f518d273056b2143f55e23deeea2813 (patch) | |
| tree | 3376811ee5d80bb779477551b3d524bcc1b417bd | |
| parent | 668c2edc15aad38229eb46c022571df2cbf31079 (diff) | |
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.
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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) |