From 6817b634825638e6ff6c0b41dbc61f8410c55f43 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 22 Aug 2019 00:58:51 +0200
Subject: [declare] Use helper function for `fix_exn` instead of relying on
 internals.

---
 vernac/declareDef.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac/declareDef.ml')

diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index f044c025d8..e57c324c9a 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -44,7 +44,7 @@ end
 
 (* Locality stuff *)
 let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
-  let fix_exn = Future.fix_exn_of ce.proof_entry_body in
+  let fix_exn = Declare.Internal.get_fix_exn ce in
   let gr = match scope with
   | Discharge ->
       let () =
-- 
cgit v1.2.3