Support compilation using [dune].

Rodolphe Lepigre · liyishuai · commit 67db2e0e81bf · 2024-09-03T23:35:29.000+08:00
diff --git a/.gitignore b/.gitignore
@@ -1,3 +1,4 @@
+_build/
 *.vo
 *.glob
 *.v.d
diff --git a/dune-project b/dune-project
@@ -0,0 +1,2 @@
+(lang dune 3.8)
+(using coq 0.8)
diff --git a/examples/dune 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
@@ -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
@@ -0,0 +1,4 @@
+(include_subdirs qualified)
+(coq.theory
+ (name ExtLib)
+ (package coq-ext-lib))

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-Require Import List String.`
	`1`	`+From Coq Require Import List String.`
`2`	`2`	`Require Import ExtLib.Structures.CoMonad.`
`3`	`3`
`4`	`4`	`Set Implicit Arguments.`