From 045913a5bf299f033b82d377dff4e79b288f9b07 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Mon, 5 Feb 2024 19:12:09 +0100
Subject: [PATCH] [compat] Release 0.1.8 for Coq 8.19

---
 Makefile               |  9 +++------
 controller/rq_hover.ml |  2 +-
 coq-lsp.opam           | 19 +++----------------
 3 files changed, 7 insertions(+), 23 deletions(-)

diff --git a/Makefile b/Makefile
index 46545849..f96520f3 100644
--- a/Makefile
+++ b/Makefile
@@ -1,10 +1,6 @@
 COQ_BUILD_CONTEXT=../_build/default/coq
 
-PKG_SET= \
-vendor/coq/coq-core.install \
-vendor/coq/coq-stdlib.install \
-vendor/coq-serapi/coq-serapi.install \
-coq-lsp.install
+PKG_SET= coq-lsp.install
 
 # Get the ocamlformat version from the .ocamlformat file
 OCAMLFORMAT=ocamlformat.$$(awk -F = '$$1 == "version" {print $$2}' .ocamlformat)
@@ -71,7 +67,8 @@ winconfig:
 	&& cp user-contrib/Ltac2/dune.disabled user-contrib/Ltac2/dune
 
 .PHONY: coq_boot
-coq_boot: vendor/coq/config/coq_config.ml
+coq_boot:
+# coq_boot: vendor/coq/config/coq_config.ml
 
 .PHONY: clean
 clean:
diff --git a/controller/rq_hover.ml b/controller/rq_hover.ml
index 6d600f91..e680f83f 100644
--- 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/coq-lsp.opam b/coq-lsp.opam
index be63834d..abec7203 100644
--- a/coq-lsp.opam
+++ b/coq-lsp.opam
@@ -19,7 +19,7 @@ doc: "https://ejgallego.github.io/coq-lsp/"
 
 depends: [
   "ocaml"        { >= "4.11.0" }
-  "dune"         { >= "3.5.0" & < "3.8.0" } # This is 3.2.0 for non-composed builds
+  "dune"         { >= "3.2.0" }
 
   # lsp dependencies
   "cmdliner"     { >= "1.1.0" }
@@ -31,21 +31,8 @@ depends: [
   "menhir"       { >= "20220210" }
 
   # Uncomment this for releases
-  # "coq"          { >= "8.17" < "8.18"  }
-  # "coq-serapi"   { >= "8.17" < "8.18"  }
-
-  # coq deps: remove this for releases
-  "ocamlfind" {>= "1.8.1"}
-  "zarith" {>= "1.11"}
-
-  # serapi deps: remove this for releases
-  "ppx_deriving"        { >= "4.2.1"    }
-  "ppx_deriving_yojson" { >= "3.4"      }
-  "ppx_import"          { >= "1.5-3"    }
-  "sexplib"             { >= "v0.13.0" & < "v0.17" }
-  "ppx_sexp_conv"       { >= "v0.13.0" & < "v0.17" }
-  "ppx_compare"         { >= "v0.13.0" & < "v0.17" }
-  "ppx_hash"            { >= "v0.13.0" & < "v0.17" }
+  "coq"          { >= "8.19" < "8.20"  }
+  "coq-serapi"   { >= "8.19" < "8.20"  }
 ]
 
 build: [ [ "dune" "build" "-p" name "-j" jobs ] ]