aboutsummaryrefslogtreecommitdiffstats
path: root/extraction/main.ml
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-02-13 12:03:45 +0000
committerYann Herklotz <git@yannherklotz.com>2020-02-13 12:03:45 +0000
commitf53038c5a4fd3fdab8233e57c84f1dc43dcf9425 (patch)
treea5d066af53746149c47ed0a33c60c3f7b8dbd6af /extraction/main.ml
parent41513c2568025bda74a9ddf9e90e848cd810525f (diff)
downloadvericert-kvx-f53038c5a4fd3fdab8233e57c84f1dc43dcf9425.tar.gz
vericert-kvx-f53038c5a4fd3fdab8233e57c84f1dc43dcf9425.zip
Improve the Coq sources and add extraction
Diffstat (limited to 'extraction/main.ml')
-rw-r--r--extraction/main.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/extraction/main.ml b/extraction/main.ml
index 235a155..870a0bc 100644
--- a/extraction/main.ml
+++ b/extraction/main.ml
@@ -6,4 +6,4 @@ let rec nat_to_int = function
| S n -> 1 + nat_to_int n
let () =
- print_endline ("Result: " ^ (Verilog.value_to_nat (Verilog.VBool Coq_true) |> nat_to_int))
+ print_endline ("Result: ")