Skip to content

Commit 4e1662f

Browse files
authored
Merge pull request #2339 from Alizter/push-stnmyvypstvk
chore: bump minimal rocq version
2 parents 51ccaaf + 4116efc commit 4e1662f

File tree

2 files changed

+4
-3
lines changed

2 files changed

+4
-3
lines changed

coq-hott.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@
22
opam-version: "2.0"
33
synopsis: "The Homotopy Type Theory library"
44
description: """
5-
To use the HoTT library, the following flags must be passed to coqc:
5+
To use the HoTT library, the following flags must be passed to rocq:
66
-noinit -indices-matter
77
To use the HoTT library in a project, add the following to _CoqProject:
88
-arg -noinit

dune-project

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,5 +23,6 @@
2323
(name coq-hott)
2424
(synopsis "The Homotopy Type Theory library")
2525
(description
26-
"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")
27-
(depends))
26+
"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")
27+
(depends
28+
(rocq (>= 9.0.0))))

0 commit comments

Comments
 (0)