diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-08-19 19:51:02 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-08-19 19:51:02 +0000 |
| commit | be6ee173206a929ad664ff507334ad5add7ad157 (patch) | |
| tree | bfc3228af152a38598bc09798c5602d5e5953148 /contrib | |
| 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 'contrib')
| -rw-r--r-- | contrib/extraction/haskell.ml | 4 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 2 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index a3e0aa12f..8859ebc7a 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 c55d3746f..5c842f159 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 dfc0d2765..f9b91d226 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)) |