diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coqc.ml | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index 5710b97f2a..e7239da682 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -30,13 +30,8 @@ let verbose = ref false let rec make_compilation_args = function | [] -> [] | file :: fl -> - let file_noext = - if Filename.check_suffix file ".v" then - Filename.chop_suffix file ".v" - else file - in (if !verbose then "-compile-verbose" else "-compile") - :: file_noext :: (make_compilation_args fl) + :: file :: (make_compilation_args fl) (* compilation of files [files] with command [command] and args [args] *) |