Sur le conseil de X.Leroy: x=[||] devient Array.length x=0

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7305 85f007b7-540e-0410-9357-904b9bb8a0f7

10 files changed, 17 insertions, 15 deletions

diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index a3e0aa12fb..8859ebc7a9 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -217,11 +217,11 @@ let pp_one_ind ip pl cv =
       	       	prlist_with_sep 
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
-  str (if cv = [||] then "type " else "data ") ++ 
+  str (if Array.length cv = 0 then "type " else "data ") ++ 
   pp_global (IndRef ip) ++ str " " ++
   prlist_with_sep (fun () -> str " ") pr_lower_id pl ++
   (if pl = [] then mt () else str " ") ++
-  if cv = [||] then str "= () -- empty inductive"
+  if Array.length cv = 0 then str "= () -- empty inductive"
   else 
     (v 0 (str "= " ++
 	  prvect_with_sep (fun () -> fnl () ++ str "  | ") pp_constructor 
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index c55d3746f7..5c842f159c 100644
--- a/contrib/extraction/mlutil.ml
+++ b/contrib/extraction/mlutil.ml
@@ -655,7 +655,7 @@ let check_generalizable_case unsafe br =
 (*s Do all branches correspond to the same thing? *)
 
 let check_constant_case br = 
-  if br = [||] then raise Impossible; 
+  if Array.length br = 0 then raise Impossible; 
   let (r,l,t) = br.(0) in
   let n = List.length l in 
   if ast_occurs_itvl 1 n t then raise Impossible; 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index dfc0d27653..f9b91d2269 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -409,7 +409,7 @@ let pp_one_ind prefix ip pl cv =
 			(fun () -> spc () ++ str "* ") (pp_type true pl) l))
   in
   pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ 
-  if cv = [||] then str " unit (* empty inductive *)" 
+  if Array.length cv = 0 then str " unit (* empty inductive *)" 
   else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor
 			(Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv))
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 40965d2f59..7877fbccbf 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -453,7 +453,7 @@ and compile_str_cst reloc sc sz cont =
       let nargs = Array.length args in
       comp_args compile_str_cst reloc args sz (Kmakeblock(nargs,tag) :: cont)
   | Bconstruct_app(tag,nparams,arity,args) ->
-      if args = [||] then code_construct tag nparams arity cont
+      if Array.length args = 0 then code_construct tag nparams arity cont
       else
 	comp_app 
 	  (fun _ _ _ cont -> code_construct tag nparams arity cont) 
diff --git a/kernel/term.ml b/kernel/term.ml
index e62b10b791..b86ac850cd 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -226,7 +226,7 @@ let mkLetIn (x,c1,t,c2) = LetIn (x,c1,t,c2)
 (* We ensure applicative terms have at least one argument and the
    function is not itself an applicative term *)
 let mkApp (f, a) = 
-  if a=[||] then f else
+  if Array.length a = 0 then f else
     match f with
       | App (g, cl) -> App (g, Array.append cl a)
       | _ -> App (f, a)
@@ -435,7 +435,7 @@ let rec collapse_appl c = match kind_of_term c with
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| Cast (c,_) when isApp c -> collapse_rec c cl2
-	| _ -> if cl2 = [||] then f else mkApp (f,cl2)
+	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
   | _ -> c
@@ -451,7 +451,7 @@ let rec strip_head_cast c = match kind_of_term c with
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| Cast (c,_) -> collapse_rec c cl2
-	| _ -> if cl2 = [||] then f else mkApp (f,cl2)
+	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
   | Cast (c,t) -> strip_head_cast c
diff --git a/lib/bigint.ml b/lib/bigint.ml
index 40e04cc342..680424275a 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -75,10 +75,11 @@ let normalize_neg n =
   let k = ref 1 in
   while !k < Array.length n & n.(!k) = base - 1 do incr k done;
   let n' = Array.sub n !k (Array.length n - !k) in
-  if n' = [||] then [|-1|] else (n'.(0) <- n'.(0) - base; n')
+  if Array.length n' = 0 then [|-1|] else (n'.(0) <- n'.(0) - base; n')
 
 let rec normalize n =
-  if n=[||] then n else if n.(0) = -1 then normalize_neg n else normalize_pos n
+  if Array.length n = 0 then n else 
+    if n.(0) = -1 then normalize_neg n else normalize_pos n
 
 let neg m =
   if m = zero then zero else
@@ -254,7 +255,7 @@ let of_string s =
   a
 
 let to_string_pos sgn n =
-   if n = [||] then "0" else
+   if Array.length n = 0 then "0" else
      sgn ^
      String.concat ""
       (string_of_int n.(0) :: List.map format_size (List.tl (Array.to_list n)))
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0f079bcf95..d80fd80758 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1336,7 +1336,7 @@ and match_current pb ((current,typ as ct),deps) =
 	let mind,_ = dest_ind_family indf in
 	let cstrs = get_constructors pb.env indf in
 	let eqns,onlydflt = group_equations pb mind current cstrs pb.mat in
-	if (cstrs <> [||] or pb.mat <> []) & onlydflt  then
+	if (Array.length cstrs <> 0 or pb.mat <> []) & onlydflt  then
 	  compile (shift_problem ct pb)
 	else
           let constraints = Array.map (solve_constraints indt) cstrs in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 880605313a..9dc25a0b56 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -224,7 +224,8 @@ let detype_case computable detype detype_eqn testdep
   let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
   let consnargsl = Array.map List.length consnargs in
   let alias, aliastyp, newpred, pred = 
-    if (not !Options.raw_print) & synth_type & computable & bl <> [||] then
+    if (not !Options.raw_print) & synth_type & computable & Array.length bl<>0 
+    then 
       Anonymous, None, None, None
     else
       let p = option_app detype p in
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index 0eefa24423..ee1bfe4d60 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -263,7 +263,7 @@ let rec strip_head_cast c = match kind_of_term c with
       let rec collapse_rec f cl2 = match kind_of_term f with
 	| App (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| Cast (c,_) -> collapse_rec c cl2
-	| _ -> if cl2 = [||] then f else mkApp (f,cl2)
+	| _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
   | Cast (c,t) -> strip_head_cast c
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 7a3e39e94b..3db8be9dcb 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -633,7 +633,7 @@ let apply_to_rels c l =
    applistc c (Util.list_map_i (fun i _ -> mkRel (len - i)) 0 l)
 
 let apply_to_relation subst rel =
- if subst = [||] then rel
+ if Array.length subst = 0 then rel
  else
   let new_quantifiers_no = rel.rel_quantifiers_no - Array.length subst in
    assert (new_quantifiers_no >= 0) ;