From a1c5f39b542118aef049f8e8fb1454d142095471 Mon Sep 17 00:00:00 2001
From: Yann Leray <yann.leray@inria.fr>
Date: Thu, 8 Feb 2024 17:56:47 +0100
Subject: [PATCH] Fix relevance on symbols

---
 kernel/constant_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/constant_typing.ml b/kernel/constant_typing.ml
index f1b3e2097cb7..a606df2ec82a 100644
--- a/kernel/constant_typing.ml
+++ b/kernel/constant_typing.ml
@@ -183,7 +183,7 @@ let infer_symbol env { symb_entry_universes; symb_entry_unfold_fix; symb_entry_t
     const_type = t;
     const_body_code = None;
     const_universes = univs;
-    const_relevance = r;
+    const_relevance = UVars.subst_sort_level_relevance usubst r;
     const_inline_code = false;
     const_typing_flags = Environ.typing_flags env;
   }