extraction via dune, while keeping compatibility with coq_makefile

coq-community · May 27, 2020 · 8bc4511 · 8bc4511
1 parent 09db845
commit 8bc4511
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 5 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -10,7 +10,6 @@ theories/Buch.v
 theories/CoefStructure.v
 theories/Dickson.v
 theories/DivTerm.v
-theories/Extract.v
 theories/Fred.v
 theories/LetP.v
 theories/LexiOrder.v
@@ -34,3 +33,4 @@ theories/Pspminus.v
 theories/Pspoly.v
 theories/Term.v
 theories/WfR0.v
+src/Extract.v
diff --git a/dune-project b/dune-project
@@ -1,3 +1,3 @@
-(lang dune 2.4)
-(using coq 0.1)
+(lang dune 2.5)
+(using coq 0.2)
 (name coq-buchberger)
diff --git a/theories/Extract.v → src/Extract.v b/theories/Extract.v → src/Extract.v
@@ -9,8 +9,8 @@
 (*                                                                           *)
 (*****************************************************************************)
 
-Require Import LexiOrder.
-Require Import BuchRed.
+Require Import Buchberger.LexiOrder.
+Require Import Buchberger.BuchRed.
 Require Extraction.
 
 Extraction

diff --git a/src/dune b/src/dune
@@ -0,0 +1,5 @@
+(coq.extraction
+ (prelude Extract)
+ (extracted_modules sin_num)
+ (theories Buchberger)
+ (flags -w -extraction-opaque-accessed))