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.

---
 library/declare.ml  | 4 ++--
 library/declare.mli | 3 ++-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index 63e5a72245..5968fbf38b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -225,9 +225,9 @@ let declare_constant_common id cst =
   update_tables c;
   c
 
-let definition_entry ?(opaque=false) ?(inline=false) ?types
+let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
-  { const_entry_body = Future.from_val ((body,Univ.ContextSet.empty), eff);
+  { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
     const_entry_polymorphic = poly;
diff --git a/library/declare.mli b/library/declare.mli
index fdbd235614..c6119a58ac 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -48,7 +48,8 @@ type internal_flag =
   | UserIndividualRequest
 
 (* Defaut definition entries, transparent with no secctx or proj information *)
-val definition_entry : ?opaque:bool -> ?inline:bool -> ?types:types -> 
+val definition_entry : ?fix_exn:Future.fix_exn ->
+  ?opaque:bool -> ?inline:bool -> ?types:types ->
   ?poly:polymorphic -> ?univs:Univ.universe_context ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
-- 
cgit v1.2.3