Merge PR #10406: Desynchronize the type of proof and kernel entries

Reviewed-by: ejgallego
Reviewed-by: gares

1 files changed, 2 insertions, 2 deletions

diff --git a/engine/uState.ml b/engine/uState.ml
index 6a1282203a..bd61112f08 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -452,9 +452,9 @@ let restrict ctx vars =
   let uctx' = restrict_universe_context ctx.uctx_local vars in
   { ctx with uctx_local = uctx' }
 
-let demote_seff_univs entry uctx =
+let demote_seff_univs universes uctx =
   let open Entries in
-  match entry.const_entry_universes with
+  match universes with
   | Polymorphic_entry _ -> uctx
   | Monomorphic_entry (univs, _) ->
     let seff = LSet.union uctx.uctx_seff_univs univs in