diff options
| -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: ") |