aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--driver/CoqupDriver.ml20
1 files changed, 3 insertions, 17 deletions
diff --git a/driver/CoqupDriver.ml b/driver/CoqupDriver.ml
index 8363ca5..3dd0ed1 100644
--- a/driver/CoqupDriver.ml
+++ b/driver/CoqupDriver.ml
@@ -27,7 +27,6 @@
*)
open Printf
-open Coqup.Camlcoq
open Coqup.Commandline
open Coqup.Clflags
open Coqup.CommonOptions
@@ -100,22 +99,9 @@ let compile_c_file sourcename ifile ofile =
| Coqup.Errors.Error msg ->
let loc = file_loc sourcename in
fatal_error loc "%a" print_error msg in
- if not !option_simulate then begin
- let oc = open_out ofile in
- Coqup.PrintVerilog.print_program oc verilog;
- close_out oc
- end else begin
- let result, state =
- match Coqup.Simulator.simulate (Nat.of_int 100) verilog with
- | Coqup.Errors.OK r -> r
- | Coqup.Errors.Error msg ->
- let loc = file_loc sourcename in
- fatal_error loc "%a" print_error msg in
- Coqup.PrintVerilog.print_result stdout state;
- print_string "Result: ";
- Coqup.PrintVerilog.print_value stdout result;
- print_newline ()
- end
+ let oc = open_out ofile in
+ Coqup.PrintVerilog.print_program oc verilog;
+ close_out oc
end
(* From C source to asm *)