Merge PR #6469: No universe constraints in Let definitions

1 files changed, 17 insertions, 4 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index 8781c8719..5be07e09e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -231,11 +231,24 @@ 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 poly = match de.const_entry_universes with
-      | Monomorphic_const_entry _ -> false
-      | Polymorphic_const_entry _ -> true
+      (** The body should already have been forced upstream because it is a
+          section-local definition, but it's not enforced by typing *)
+      let (body, uctx), () = Future.force de.const_entry_body in
+      let poly, univs = match de.const_entry_universes with
+      | Monomorphic_const_entry uctx -> false, uctx
+      | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
       in
+      let univs = Univ.ContextSet.union uctx univs in
+      (** We must declare the universe constraints before type-checking the
+          term. *)
+      let () = Global.push_context_set (not poly) univs in
+      let se = {
+        secdef_body = body;
+        secdef_secctx = de.const_entry_secctx;
+        secdef_feedback = de.const_entry_feedback;
+        secdef_type = de.const_entry_type;
+      } in
+      let () = Global.push_named_def (id, se) in
       Explicit, de.const_entry_opaque,
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);