From 593e784250eca0f38479109395a5fbc605f2c3c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Oct 2019 16:00:00 +0200
Subject: Simplify future forcing in Declare.

---
 tactics/declare.ml | 2 --
 1 file changed, 2 deletions(-)

diff --git a/tactics/declare.ml b/tactics/declare.ml
index 63a93d3dc3..7d32f1a7e8 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -310,8 +310,6 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind
   let kn, eff =
     let de =
       if not de.proof_entry_opaque then
-        let body, () = Future.force de.proof_entry_body in
-        let de = { de with proof_entry_body = Future.from_val (body, ()) } in
         DefinitionEff (cast_proof_entry de)
       else
         let de = cast_opaque_proof_entry PureEntry de in
-- 
cgit v1.2.3