diff options
Diffstat (limited to 'interp/declare.ml')
| -rw-r--r-- | interp/declare.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/interp/declare.ml b/interp/declare.ml index 8781c8719..ae28c4b90 100644 --- a/interp/declare.ml +++ b/interp/declare.ml @@ -231,7 +231,15 @@ let cache_variable ((sp,_),o) = | SectionLocalDef (de) -> let (de, eff) = Global.export_private_constants ~in_section:true de in let () = List.iter register_side_effect eff in - let univs = Global.push_named_def (id,de) in + let body = Future.chain de.const_entry_body (fun (body, ()) -> body) in + let se = { + secdef_body = body; + secdef_secctx = de.const_entry_secctx; + secdef_universes = de.const_entry_universes; + secdef_feedback = de.const_entry_feedback; + secdef_type = de.const_entry_type; + } in + let univs = Global.push_named_def (id, se) in let poly = match de.const_entry_universes with | Monomorphic_const_entry _ -> false | Polymorphic_const_entry _ -> true |