From 67db2e0e81bf45709b84c51624476879b21e1487 Mon Sep 17 00:00:00 2001 From: Rodolphe Lepigre Date: Tue, 3 Sep 2024 11:57:16 +0200 Subject: [PATCH] Support compilation using [dune]. --- .gitignore | 1 + dune-project | 2 ++ examples/dune | 4 ++++ theories/Generic/Ind.v | 2 +- theories/dune | 4 ++++ 5 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 dune-project create mode 100644 examples/dune create mode 100644 theories/dune diff --git a/.gitignore b/.gitignore index d422fbe..6a08d4d 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1,4 @@ +_build/ *.vo *.glob *.v.d diff --git a/dune-project b/dune-project new file mode 100644 index 0000000..8b858cd --- /dev/null +++ b/dune-project @@ -0,0 +1,2 @@ +(lang dune 3.8) +(using coq 0.8) diff --git a/examples/dune b/examples/dune new file mode 100644 index 0000000..6217535 --- /dev/null +++ b/examples/dune @@ -0,0 +1,4 @@ +(include_subdirs qualified) +(coq.theory + (name ExtLibExamples) + (theories ExtLib)) diff --git a/theories/Generic/Ind.v b/theories/Generic/Ind.v index 2c2c620..0dab979 100644 --- a/theories/Generic/Ind.v +++ b/theories/Generic/Ind.v @@ -1,4 +1,4 @@ -Require Import List String. +From Coq Require Import List String. Require Import ExtLib.Structures.CoMonad. Set Implicit Arguments. diff --git a/theories/dune b/theories/dune new file mode 100644 index 0000000..240500e --- /dev/null +++ b/theories/dune @@ -0,0 +1,4 @@ +(include_subdirs qualified) +(coq.theory + (name ExtLib) + (package coq-ext-lib))