summaryrefslogtreecommitdiff
path: root/contrib/extraction/test/hs2v.ml
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /contrib/extraction/test/hs2v.ml
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'contrib/extraction/test/hs2v.ml')
-rw-r--r--contrib/extraction/test/hs2v.ml14
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()