aboutsummaryrefslogtreecommitdiffstats
path: root/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'extraction')
-rw-r--r--extraction/Extraction.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/extraction/Extraction.v b/extraction/Extraction.v
index 40bbe54..4c5f034 100644
--- a/extraction/Extraction.v
+++ b/extraction/Extraction.v
@@ -1,4 +1,4 @@
-Require Import Verilog.
+From CoqUp Require Import Verilog.
-Cd "src".
+Cd "extraction".
Separate Extraction Verilog.nat_to_value Verilog.value_to_nat.