aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/derive
diff options
context:
space:
mode:
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