aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/derive
diff options
context:
space:
mode:
authorGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-05-28 00:35:57 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-10-17 02:19:11 +0200
commit280be11cb4706e039cf4e9f68a5ae38b0aef9340 (patch)
treee1e1a1a8465076e0fe6e95566f14d7ea0f960813 /plugins/derive
parent19bbc3fd946555aa1fa1fc23d805a4eb3d13bc45 (diff)
[stm] Remove state-handling from Futures.
We make Vernacentries.interp functional wrt state, and thus remove state-handling from `Future`. Now, a future needs a closure if it wants to preserve state. Consequently, `Vernacentries.interp` takes a state, and returns the new one. We don't explicitly thread the state in the STM yet, instead, we recover the state that was used before and pass it explicitly to `interp`. I have tested the commit with the files in interactive, but we aware that some new bugs may appear or old ones be made more apparent. However, I am confident that this step will improve our understanding of bugs. In some cases, we perform a bit more summary wrapping/unwrapping. This will go away in future commits; informal timings for a full make: - master: real 2m11,027s user 8m30,904s sys 1m0,000s - no_futures: real 2m8,474s user 8m34,380s sys 0m59,156s
Diffstat (limited to 'plugins/derive')
-rw-r--r--plugins/derive/derive.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 1524079f4..6d3d4b743 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -10,7 +10,7 @@ open Context.Named.Declaration
let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body)
: Safe_typing.private_constants Entries.const_entry_body =
- Future.chain ~pure:true x begin fun ((b,ctx),fx) ->
+ Future.chain x begin fun ((b,ctx),fx) ->
(f b , ctx) , fx
end