aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorherbelin2006-06-08 16:39:58 +0000
committerherbelin2006-06-08 16:39:58 +0000
commit2b74dd6e10249fd91bf7a3527d980cc5fbc513aa (patch)
tree30ffb94e617fe9879ba340d69a229a25a2d693cb /tools
parent305722bfb08c576293abd27c3b0eaa18a0372403 (diff)
Warning ocaml 3.09 pour variable inutile
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8923 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdep.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index f8ee39a582..a3089f7136 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -337,7 +337,7 @@ let mL_dependencies () =
flush stdout)
(List.rev !mlAccu);
List.iter
- (fun ((name,ext,dirname) as pairname) ->
+ (fun ((name,ext,dirname)) ->
let fullname = file_name ([name],dirname) in
let (dep,_) = traite_fichier_ML fullname ext in
printf "%s.cmi: %s%s" fullname fullname ext;