aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/record.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/record.ml')
-rw-r--r--toplevel/record.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 56493bae8..af7f364f3 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -262,7 +262,7 @@ let declare_projections indsp ?(kind=StructureComponent) ?name coers fieldimpls
const_entry_secctx = None;
const_entry_type = Some projtyp;
const_entry_polymorphic = poly;
- const_entry_universes = Future.from_val ctx;
+ const_entry_universes = ctx;
const_entry_proj = projinfo;
const_entry_opaque = false;
const_entry_inline_code = false;