diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-02-14 15:48:03 +0000 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-02-14 15:48:03 +0000 |
| commit | 15097cc2577f59baf99e315c7b48c3653f5fa639 (patch) | |
| tree | a1a2576118b82282328d6c5f91310720389eb82b | |
| parent | 5a86c7bb8c274ea41716b9002189d2644eb1c8c6 (diff) | |
| download | vericert-15097cc2577f59baf99e315c7b48c3653f5fa639.tar.gz vericert-15097cc2577f59baf99e315c7b48c3653f5fa639.zip | |
Update dune file and remove main
| -rw-r--r-- | extraction/dune | 11 | ||||
| -rw-r--r-- | extraction/main.ml | 9 |
2 files changed, 8 insertions, 12 deletions
diff --git a/extraction/dune b/extraction/dune index ec44a53..12a6b8d 100644 --- a/extraction/dune +++ b/extraction/dune @@ -1,3 +1,8 @@ -(executable - (name main) - (flags (:standard -warn-error -A))) +(executables + (flags (:standard -warn-error -A)) + (names driver) + (libraries compcert)) + +(install + (section bin) + (files (driver.exe as coqup))) diff --git a/extraction/main.ml b/extraction/main.ml deleted file mode 100644 index 870a0bc..0000000 --- a/extraction/main.ml +++ /dev/null @@ -1,9 +0,0 @@ -open Verilog -open Datatypes - -let rec nat_to_int = function - | O -> 0 - | S n -> 1 + nat_to_int n - -let () = - print_endline ("Result: ") |