From 77cf18eb844b45776b2ec67be9f71e8dd4ca002c Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 30 Oct 2015 11:48:40 -0400
Subject: Add a way to get the right fix_exn in external vernacular commands
 involving Futures.

---
 toplevel/obligations.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index e488f84f8a..9019f486be 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -508,16 +508,17 @@ let declare_definition prg =
   let nf = Universes.nf_evars_and_universes_opt_subst (fun x -> None)
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
+  let fix_exn = Stm.get_fix_exn () in
   let ce =
-    definition_entry ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
-      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
+    definition_entry ~fix_exn
+     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
+     ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
     progmap_remove prg;
     !declare_definition_ref prg.prg_name 
       prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r ->
-         Lemmas.call_hook (fun exn -> exn) prg.prg_hook l r; r))
-
+      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r; r))
+      
 open Pp
 
 let rec lam_index n t acc =
@@ -618,8 +619,9 @@ let declare_obligation prg obl body ty uctx =
 	if get_shrink_obligations () && not poly then
 	  shrink_body body else [], body, [||] 
       in
+      let body = ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
       let ce = 
-        { const_entry_body = Future.from_val((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants);
+        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
           const_entry_secctx = None;
 	  const_entry_type = if List.is_empty ctx then ty else None;
 	  const_entry_polymorphic = poly;
-- 
cgit v1.2.3


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(-)

(limited to 'toplevel')

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 73fd3d1a4a..3d338ee0a3 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