From ad380aca8cad3329c9a3db4b65b933b1179ed6a2 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 14 Apr 2021 14:09:07 +0200
Subject: Cleanup useless environment manipulation in Class declaration

---
 vernac/record.ml | 4 +---
 1 file changed, 1 insertion(+), 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;
-- 
cgit v1.2.3