diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 12:15:09 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-19 12:15:09 +0000 |
commit | 1f009ebf50eb1e697698b5ca95bdbdda56cee8f9 (patch) | |
tree | 81eccd4e1fc2cfc12fc854185e1b36c30306b62e /contrib/extraction/test/ml2v.ml | |
parent | ecb6f948a27b96d21fd55d4ba0d214a55b48740e (diff) |
script de bench automatique pour extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1615 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test/ml2v.ml')
-rw-r--r-- | contrib/extraction/test/ml2v.ml | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml new file mode 100644 index 000000000..665aabba4 --- /dev/null +++ b/contrib/extraction/test/ml2v.ml @@ -0,0 +1,17 @@ +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();; + |