Merge PR #14112: Cleanup useless environment manipulation in Class declaration

Reviewed-by: ejgallego

1 files changed, 1 insertions, 3 deletions

diff --git a/vernac/record.ml b/vernac/record.ml
index fccc3e4fbd..53f3508806 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -766,11 +766,9 @@ let add_inductive_class env sigma ind =
   let k =
     let ctx = oneind.mind_arity_ctxt in
     let univs = Declareops.inductive_polymorphic_context mind in
-    let env = push_context ~strict:false (Univ.AUContext.repr univs) env in
-    let env = push_rel_context ctx env in
     let inst = Univ.make_abstract_instance univs in
     let ty = Inductive.type_of_inductive ((mind, oneind), inst) in
-    let r = Inductive.relevance_of_inductive env ind in
+    let r = oneind.mind_relevance in
       { cl_univs = univs;
         cl_impl = GlobRef.IndRef ind;
         cl_context = ctx;