Merge pull request #549 from SkySkimmer/sort-poly

Adapt to coq/coq#17836 (sort poly)
ejgallego · Nov 7, 2023 · 53e12d3 · 53e12d3
2 parents e319c94 + ce3f9f5
commit 53e12d3
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 3 deletions.
diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml
@@ -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

diff --git a/vendor/coq b/vendor/coq
diff --git a/vendor/coq-serapi b/vendor/coq-serapi