[compat] Release 0.1.8 for Coq 8.19

ejgallego · Feb 5, 2024 · 045913a · 045913a
1 parent 550a4a4
commit 045913a
Show file tree

Hide file tree

Showing 3 changed files with 7 additions and 23 deletions.
diff --git 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
@@ -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
@@ -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 ] ]