1 files changed, 13 insertions, 17 deletions
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml
index 665aabba4a..f891b40ff0 100644
--- a/contrib/extraction/test/ml2v.ml
+++ b/contrib/extraction/test/ml2v.ml
@@ -1,17 +1,13 @@
-let main () = begin
-  let j = Array.length (Sys.argv) in
-  if j>0 then begin
-	let s = Sys.argv.(1) in
-	let b = Filename.chop_extension (Filename.basename s) in 
-	let b0 = String.sub b 0 1 in
-	let b1 = String.capitalize b0 in  
-	let b = String.sub b 1 ((String.length b) -1) in 
-	let d = Filename.dirname s
-	in print_string (d^"/["^b0^b1^"]"^b^".v");
-	print_newline()
-  end;
-  exit(0)	
-end;;	
-
-main();;
- 		
+let _ =
+  let j = Array.length Sys.argv in
+  if j > 0 then
+    let fml = Sys.argv.(1) in
+    let f = Filename.chop_extension fml in 
+    let fv = f ^ ".v" in
+    if Sys.file_exists fv then
+      print_endline fv
+    else
+      let d = Filename.dirname f in
+      let b = String.capitalize (Filename.basename f) in
+      let fv = Filename.concat d (b ^ ".v") in
+      print_endline fv