diff options
| author | letouzey | 2005-08-19 21:32:46 +0000 |
|---|---|---|
| committer | letouzey | 2005-08-19 21:32:46 +0000 |
| commit | e31434db0bd91d4c6b3fec8ad09b74c3613630a0 (patch) | |
| tree | 239f85961ff86c93e7135580124a319bf0850fe5 | |
| 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
| -rw-r--r-- | contrib/xml/cic2acic.ml | 2 | ||||
| -rw-r--r-- | lib/profile.ml | 2 | ||||
| -rw-r--r-- | parsing/prettyp.ml | 2 | ||||
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | tools/coqdoc/main.ml | 2 |
5 files changed, 5 insertions, 5 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index a0faa6426e..54510ba179 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -697,7 +697,7 @@ print_endline "PASSATO" ; flush stdout ; let compute_result_if_eta_expansion_not_required subst residual_args = - let residual_args_not_empty = List.length residual_args > 0 in + let residual_args_not_empty = residual_args <> [] in let h' = if residual_args_not_empty then aux' env idrefs ~subst:(None,subst) h diff --git a/lib/profile.ml b/lib/profile.ml index cce4ecd318..1197c92a91 100644 --- a/lib/profile.ml +++ b/lib/profile.ml @@ -328,7 +328,7 @@ let close_profile print = outside.owntime <- outside.owntime + t; ajoute_ownalloc outside dw; ajoute_totalloc outside dw; - if List.length !prof_table <> 0 then begin + if !prof_table <> [] then begin let ov_bc = time_overhead_B_C () (* B+C overhead *) in let ov_ad = time_overhead_A_D () (* A+D overhead *) in let adjust (n,e) = (n, adjust_time ov_bc ov_ad e) in diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 2122e3a8f9..ac5c7430ff 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -267,7 +267,7 @@ let assumptions_for_print lna = (* *) let print_params env params = - if List.length params = 0 then + if params = [] then (mt ()) else if !Options.v7 then diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d80fd80758..79b048979d 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1436,7 +1436,7 @@ let rename_env subst env = let is_dependent_indtype = function | NotInd _ -> false - | IsInd (_, IndType(_,realargs)) -> List.length realargs <> 0 + | IsInd (_, IndType(_,realargs)) -> realargs <> [] let prepare_initial_alias_eqn isdep tomatchl eqn = let (subst, pats) = diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml index 8a129e7f70..820ad8240d 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 () |