summaryrefslogtreecommitdiff
path: root/contrib/extraction/test/hs2v.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/test/hs2v.ml')
-rw-r--r--contrib/extraction/test/hs2v.ml14
1 files changed, 14 insertions, 0 deletions
diff --git a/contrib/extraction/test/hs2v.ml b/contrib/extraction/test/hs2v.ml
new file mode 100644
index 00000000..fd8b9b26
--- /dev/null
+++ b/contrib/extraction/test/hs2v.ml
@@ -0,0 +1,14 @@
+let _ =
+ for j = 1 to ((Array.length Sys.argv)-1) do
+ let fml = Sys.argv.(j) in
+ let f = Filename.chop_extension fml in
+ let fv = f ^ ".v" in
+ if Sys.file_exists ("../../../" ^ fv) then
+ print_string (fv^" ")
+ else
+ let d = Filename.dirname f in
+ let b = String.uncapitalize (Filename.basename f) in
+ let fv = Filename.concat d (b ^ ".v ") in
+ print_string fv
+ done;
+ print_newline()