diff options
author | 2005-08-19 21:32:46 +0000 | |
---|---|---|
committer | 2005-08-19 21:32:46 +0000 | |
commit | e31434db0bd91d4c6b3fec8ad09b74c3613630a0 (patch) | |
tree | 239f85961ff86c93e7135580124a319bf0850fe5 /tools | |
parent | be6ee173206a929ad664ff507334ad5add7ad157 (diff) |
pas besoin de List.length pour savoir si une liste est vide
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7306 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-rw-r--r-- | tools/coqdoc/main.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 8a129e7f7..820ad8240 100644 --- a/tools/coqdoc/main.ml +++ b/tools/coqdoc/main.ml @@ -415,6 +415,6 @@ let produce_output fl = let main () = let files = parse () in if not !quiet then banner (); - if List.length files > 0 then produce_output files + if files <> [] then produce_output files let _ = Printexc.catch main () |