[upstream] Adapt to coq/coq#17836 (sort poly)

SkySkimmer · Nov 7, 2023 · 4cd466e · 4cd466e
1 parent dc242bb
commit 4cd466e
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
@@ -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

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