Skip to content

Commit

Permalink
[upstream] Adapt to coq/coq#17836 (sort poly)
Browse files Browse the repository at this point in the history
  • Loading branch information
SkySkimmer authored and ejgallego committed Nov 7, 2023
1 parent e319c94 commit ce3f9f5
Show file tree
Hide file tree
Showing 3 changed files with 3 additions and 3 deletions.
2 changes: 1 addition & 1 deletion controller/rq_hover.ml
Expand Up @@ -17,7 +17,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
2 changes: 1 addition & 1 deletion vendor/coq
Submodule coq updated 336 files

0 comments on commit ce3f9f5

Please sign in to comment.