Skip to content

Commit 9d32950

Browse files
committed
update for Coq 8.17 and Dune-Coq 0.8
1 parent c0cc512 commit 9d32950

File tree

4 files changed

+11
-15
lines changed

4 files changed

+11
-15
lines changed

coq-my-plugin.opam

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ homepage: "https://github.com/your-github/my-plugin"
55
dev-repo: "git+https://github.com/your-github/my-plugin.git"
66
bug-reports: "https://github.com/your-github/my-plugin/issues"
77
doc: "https://your-github.github.io/my-plugin"
8-
license: "MIT"
8+
license: "SPDX-identifier-for-your-license"
99

1010
synopsis: "One line description of your plugin"
1111
description: """
@@ -14,9 +14,9 @@ cover multiple lines. Including punctuation."""
1414

1515
build: ["dune" "build" "-p" name "-j" jobs]
1616
depends: [
17-
"ocaml" {>= "4.07.1"}
18-
"dune" {>= "2.5"}
19-
"coq" {>= "8.14" & < "8.15"}
17+
"ocaml" {>= "4.09.0"}
18+
"dune" {>= "3.8.2"}
19+
"coq" {>= "8.17"}
2020
]
2121

2222
tags: [

dune-project

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,3 @@
1-
(lang dune 2.9)
2-
(using coq 0.3)
1+
(lang dune 3.8)
2+
(using coq 0.8)
33
(name my-plugin)

src/dune

Lines changed: 4 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -10,18 +10,14 @@
1010

1111
(synopsis "My Coq plugin") ; Synopsis, used in META generation.
1212

13-
(flags :standard -rectypes -w -27) ; Coq requires the `-rectypes`
14-
; flag; CoqPP generated code
15-
; requires to disable warning 27
16-
; often.
13+
(flags :standard -w -27) ; CoqPP generated code requires to
14+
; disable warning 27 often.
1715

18-
(foreign_stubs ; we link our plugin with a C
16+
(foreign_stubs ; We link our plugin with a C
1917
(language c) ; library! Optional, of course.
2018
(names ce_get))
2119

22-
(libraries ; OCaml Libraries we want to link
23-
; with, your choice here.
24-
20+
(libraries ; OCaml libraries we want to link with
2521
coq-core.vernac ; Needed for vernac extend.
2622
coq-core.plugins.ltac ; Needed for tactic extend.
2723
)

theories/dune

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@
77
(package coq-my-plugin) ; Adding this line will make your
88
; library installable in the opam package
99

10-
(libraries coq-my-plugin.plugin)) ; Here you should declare all
10+
(plugins coq-my-plugin.plugin)) ; Here you should declare all
1111
; OCaml plugin dependencies
1212
; for your Coq files.
1313

0 commit comments

Comments
 (0)