Merge pull request #2297 from Alizter/no-stdlib

don't depend on coq stdlib for Rocq >= 9.0

Author: jdchristensen

coq-hott.opam

@@ -15,11 +15,6 @@ authors: ["The HoTT Library Development Team"]
 license: "BSD-2-Clause"
 homepage: "http://homotopytypetheory.org/"
 bug-reports: "https://github.com/HoTT/HoTT/issues"
-depends: [
-  "dune" {>= "3.13"}
-  "coq" {>= "8.19.0"}
-  "odoc" {with-doc}
-]
 build: [
   ["dune" "subst"] {dev}
   [
@@ -35,3 +30,7 @@ build: [
   ]
 ]
 dev-repo: "git+https://github.com/HoTT/HoTT.git"
+depends: [
+  "dune" {>= "3.13"}
+  (("rocq-core" {>= "9.0"} & "coq-core" {>= "9.0"}) | "coq" {>= "8.19.0" & < "9~"})
+]

coq-hott.opam.template

@@ -0,0 +1,4 @@
+depends: [
+  "dune" {>= "3.13"}
+  (("rocq-core" {>= "9.0"} & "coq-core" {>= "9.0"}) | "coq" {>= "8.19.0" & < "9~"})
+]

dune-project

@@ -24,6 +24,4 @@
  (synopsis "The Homotopy Type Theory library")
  (description
   "To use the HoTT library, the following flags must be passed to coqc:\n  -noinit -indices-matter\nTo use the HoTT library in a project, add the following to _CoqProject:\n  -arg -noinit\n  -arg -indices-matter\n")
- (depends
-  (coq
-   (>= 8.19.0))))
+ (depends))