Skip to content

Commit

Permalink
Adapt to coq/coq#17836 (sort poly)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer committed Sep 22, 2023
1 parent dc242bb commit c19ae78
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion controller/rq_hover.ml
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ type id_info =
let info_of_ind env sigma ((sp, i) : Names.Ind.t) =
let mib = Environ.lookup_mind sp env in
let u =
Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib)
UVars.make_abstract_instance (Declareops.inductive_polymorphic_context mib)
in
let mip = mib.Declarations.mind_packets.(i) in
let paramdecls = Inductive.inductive_paramdecls (mib, u) in
Expand Down

0 comments on commit c19ae78

Please sign in to comment.