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))