diff options
Diffstat (limited to 'interp/discharge.ml')
| -rw-r--r-- | interp/discharge.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/discharge.ml b/interp/discharge.ml index 5b4b5f67b..75bfca307 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -78,8 +78,8 @@ let refresh_polymorphic_type_of_inductive (_,mip) = let ctx = List.rev mip.mind_arity_ctxt in mkArity (List.rev ctx, Type ar.template_level), true -let process_inductive (section_decls,_,_ as info) modlist mib = - let section_decls = Lib.named_of_variable_context section_decls in +let process_inductive info modlist mib = + let section_decls = Lib.named_of_variable_context info.Lib.abstr_ctx in let nparamdecls = Context.Rel.length mib.mind_params_ctxt in let subst, ind_univs = match mib.mind_universes with |