From 58521e6066974833bb83e98a6bb17feb0c1fee90 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Sat, 21 Mar 2015 09:45:57 +0100 Subject: Do not revert parameter lists when extracting singleton types to Haskell. (Fix for bugs #3470 and #3694) --- plugins/extraction/haskell.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/extraction/haskell.ml') diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 5e08fef5f..d8eda87d6 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -243,12 +243,12 @@ let pp_logical_ind packet = prvect_with_sep spc pr_id packet.ip_consnames) let pp_singleton kn packet = + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in - let l' = List.rev l in - hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ + hov 2 (str "type " ++ name ++ spc () ++ prlist_with_sep spc pr_id l ++ (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ - pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++ + pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) -- cgit v1.2.3