from scratch

_CoqProject

@@ -0,0 +1,5 @@
+-R _build/default/theories MyPlugin
+-I _build/default/src
+# src/META.clash-extr
+# -R theories/ Clashextr
+# -I src

coq-my-plugin.opam

@@ -0,0 +1,21 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+license: "Apache-2.0"
+depends: [
+  "dune" {>= "3.6"}
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+]

dune-project

@@ -0,0 +1,8 @@
+(lang dune 3.6)
+(using coq 0.6)
+(license Apache-2.0)
+
+(generate_opam_files true)
+(package
+ (name coq-my-plugin)
+ (allow_empty))

src/dune

@@ -0,0 +1,10 @@
+; https://github.com/coq-community/coq-plugin-template/blob/v8.16/src/dune
+
+(library
+ (name my_plugin)
+ (public_name coq-my-plugin.plugin)
+ (libraries
+   coq-core.vernac
+   coq-core.plugins.extraction))
+
+(coq.pp (modules g_myplugin))

src/g_myplugin.mlg

@@ -0,0 +1,5 @@
+DECLARE PLUGIN "coq-my-plugin.plugin"
+
+{
+
+}

theories/MyPlugin.v

@@ -0,0 +1 @@
+Declare ML Module "my_plugin:coq-my-plugin.plugin".

theories/Test.v

@@ -0,0 +1,2 @@
+Require Import MyPlugin.
+

theories/dune

@@ -0,0 +1,13 @@
+; https://github.com/coq-community/coq-plugin-template/blob/v8.16/src/dune
+
+(coq.theory
+ (name MyPlugin)                   ; This will determine the top-level Coq
+                                   ; module of your theory, modules will
+                                   ; be MyPlugin.A, etc., when seen from the
+                                   ; outside.
+
+ (package coq-my-plugin)
+
+ (plugins coq-my-plugin.plugin))   ; Here you should declare all
+                                   ; OCaml plugin dependencies
+                                   ; for your Coq files.