Declare: fix Future management

3 files changed, 13 insertions, 5 deletions

diff --git a/lib/future.ml b/lib/future.ml
index 690255edda..77386a1a9f 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -90,6 +90,8 @@ let uuid kx = let id, _, _ = get kx in id
 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
+
 let default_force () = raise NotReady
 let assignement ck = fun v ->
   let _, fix_exn, c = get ck in
diff --git a/lib/future.mli b/lib/future.mli
index 09d18ff269..b4eced06a9 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -84,6 +84,9 @@ val from_val : ?fix_exn:fix_exn -> 'a -> 'a computation
    the value is not just the 'a but also the global system state *)
 val from_here : ?fix_exn:fix_exn -> 'a -> 'a computation
 
+(* To get the fix_exn of a computation *)
+val fix_exn_of : 'a computation -> fix_exn
+
 (* Run remotely, returns the function to assign.  Optionally tekes a function
    that is called when forced.  The default one is to raise NotReady.
    The assignement function does not change the uuid. *)
diff --git a/library/declare.ml b/library/declare.ml
index e92225637e..4364461ef5 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -208,7 +208,7 @@ let definition_entry ?(opaque=false) ?(inline=false) ?types
 
 let declare_scheme = ref (fun _ _ -> assert false)
 let set_declare_scheme f = declare_scheme := f
-let declare_sideff se =
+let declare_sideff fix_exn se =
   let cbl, scheme = match se with
     | SEsubproof (c, cb) -> [c, cb], None
     | SEscheme (cbl, k) ->
@@ -229,7 +229,7 @@ let declare_sideff se =
     let pt, opaque = pt_opaque_of cb in
     let ty = ty_of cb in
     { cst_decl = ConstantEntry (DefinitionEntry {
-        const_entry_body = Future.from_here (pt, Declareops.no_seff);
+        const_entry_body = Future.from_here ~fix_exn (pt, Declareops.no_seff);
         const_entry_secctx = Some cb.Declarations.const_hyps;
         const_entry_type = ty;
         const_entry_opaque = opaque;
@@ -259,12 +259,15 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
     | Entries.DefinitionEntry ({
       const_entry_polymorphic = true; const_entry_body = bo } as de)
       ->
-        let pt, seff = Future.force bo in
+        let _, seff = Future.force bo in
         if Declareops.side_effects_is_empty seff then cd
         else begin
-          Declareops.iter_side_effects declare_sideff seff;
+          let seff = Declareops.uniquize_side_effects seff in
+          Declareops.iter_side_effects
+            (declare_sideff (Future.fix_exn_of bo)) seff;
           Entries.DefinitionEntry { de with
-            const_entry_body = Future.from_val (pt, Declareops.no_seff) }
+            const_entry_body = Future.chain ~pure:true bo (fun (pt, _) ->
+              pt, Declareops.no_seff) }
         end
     | _ -> cd
   in