Updating the documentation and the toolchain w.r.t. the change in -compile.

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] *)