aboutsummaryrefslogtreecommitdiffstats
path: root/src/extraction
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-04-02 22:17:32 +0100
committerYann Herklotz <git@yannherklotz.com>2020-04-02 22:17:32 +0100
commit1cdf3b8257d1fbd1ba0bff67656163ae3f153774 (patch)
treeba3f6f9dd427d96fd879e569dc73cb316233a6ff /src/extraction
parent30ed10e388ad2f3cd1812c9770cfc09913b80c50 (diff)
downloadvericert-1cdf3b8257d1fbd1ba0bff67656163ae3f153774.tar.gz
vericert-1cdf3b8257d1fbd1ba0bff67656163ae3f153774.zip
Fix extraction on linux
Diffstat (limited to 'src/extraction')
-rw-r--r--src/extraction/Extraction.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index c7ebf8e..ff0b8ba 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -164,7 +164,7 @@ Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false".
(* Needed in Coq 8.4 to avoid problems with Function definitions. *)
Set Extraction AccessOpaque.
-Cd "src/Extraction".
+Cd "src/extraction".
Separate Extraction
Verilog.module Verilog.valueToZ coqup.Compiler.transf_hls