diff options
Diffstat (limited to 'contrib/extraction/test/hs2v.ml')
-rw-r--r-- | contrib/extraction/test/hs2v.ml | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/contrib/extraction/test/hs2v.ml b/contrib/extraction/test/hs2v.ml deleted file mode 100644 index fd8b9b26..00000000 --- a/contrib/extraction/test/hs2v.ml +++ /dev/null @@ -1,14 +0,0 @@ -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() |