fix dune-project version

Alizter · Alizter · commit 6309a97ce5d9 · 2026-01-11T01:01:07.000Z
Signed-off-by: Ali Caglayan &lt;alizter@gmail.com&gt;
diff --git a/coq-hott.opam b/coq-hott.opam
@@ -15,6 +15,11 @@ 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"}
+  "rocq-core" {>= "9.0"}
+  "odoc" {with-doc}
+]
 build: [
   ["dune" "subst"] {dev}
   [
@@ -30,7 +35,3 @@ 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~"})
-]
diff --git a/coq-hott.opam.template b/coq-hott.opam.template
diff --git a/dune-project b/dune-project
@@ -25,4 +25,4 @@
  (description
   "To use the HoTT library, the following flags must be passed to rocq:\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
-  (rocq (>= 9.0.0))))
+  (rocq-core (>= 9.0))))

Original file line number	Diff line number	Diff line change
`@@ -15,6 +15,11 @@ authors: ["The HoTT Library Development Team"]`
`15`	`15`	`license: "BSD-2-Clause"`
`16`	`16`	`homepage: "http://homotopytypetheory.org/"`
`17`	`17`	`bug-reports: "https://github.com/HoTT/HoTT/issues"`
	`18`	`+depends: [`
	`19`	`+ "dune" {>= "3.13"}`
	`20`	`+ "rocq-core" {>= "9.0"}`
	`21`	`+ "odoc" {with-doc}`
	`22`	`+]`
`18`	`23`	`build: [`
`19`	`24`	`["dune" "subst"] {dev}`
`20`	`25`	`[`
`@@ -30,7 +35,3 @@ build: [`
`30`	`35`	`]`
`31`	`36`	`]`
`32`	`37`	`dev-repo: "git+https://github.com/HoTT/HoTT.git"`
`33`		`-depends: [`
`34`		`- "dune" {>= "3.13"}`
`35`		`- (("rocq-core" {>= "9.0"} & "coq-core" {>= "9.0"}) \| "coq" {>= "8.19.0" & < "9~"})`
`36`		`-]`