diff options
| author | letouzey | 2005-08-19 19:51:02 +0000 |
|---|---|---|
| committer | letouzey | 2005-08-19 19:51:02 +0000 |
| commit | be6ee173206a929ad664ff507334ad5add7ad157 (patch) | |
| tree | bfc3228af152a38598bc09798c5602d5e5953148 /pretyping | |
| parent | 66a2d880e14c1635f29cef0ad0113185cba29a18 (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 2 | ||||
| -rw-r--r-- | pretyping/detyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/termops.ml | 2 |
3 files changed, 4 insertions, 3 deletions
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 |