diff options
| author | Pierre-Marie Pédrot | 2019-10-13 16:00:00 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-16 17:46:11 +0200 |
| commit | 593e784250eca0f38479109395a5fbc605f2c3c4 (patch) | |
| tree | a1302b210a3cabbd4cc14ede051f1f17d6e7b04a | |
| parent | 221db99a7809cad8f613baa2038fbbd8fb27a691 (diff) | |
Simplify future forcing in Declare.
| -rw-r--r-- | tactics/declare.ml | 2 |
1 files changed, 0 insertions, 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 |