diff options
Diffstat (limited to 'kernel/cooking.ml')
| -rw-r--r-- | kernel/cooking.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 4c2f22199..dbe83a856 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -126,7 +126,7 @@ let on_body f = function | Undef _ as x -> x | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs))) | OpaqueDef lc -> - OpaqueDef (Future.chain ~id:"Cooking.on_body" ~pure:true lc (fun lc -> + OpaqueDef (Future.chain lc (fun lc -> (Lazyconstr.opaque_from_val (f (Lazyconstr.force_opaque lc))))) let constr_of_def = function |