diff options
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index a1a87d54e..f095a5d6c 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -79,7 +79,7 @@ let red_constant_entry n ce sigma = function let (_, c) = redfun env sigma c in EConstr.Unsafe.to_constr c in - { ce with const_entry_body = Future.chain ~pure:true proof_out + { ce with const_entry_body = Future.chain proof_out (fun ((body,ctx),eff) -> (under_binders env sigma redfun n body,ctx),eff) } let warn_implicits_in_term = |