From 3930c586507bfb3b80297d7a2fdbbc6049aa509b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Sep 2015 19:13:30 +0200
Subject: Updating the documentation and the toolchain w.r.t. the change in
 -compile.

---
 tools/coqc.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

(limited to 'tools')

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] *)
 
-- 
cgit v1.2.3