diff options
| -rw-r--r-- | vernac/record.ml | 4 |
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; |