diff options
Diffstat (limited to 'contrib/extraction/haskell.ml')
| -rw-r--r-- | contrib/extraction/haskell.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 3834fe81..c4ed364a 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*) +(*i $Id: haskell.ml 7653 2005-12-16 04:12:26Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -240,11 +240,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 |