diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-21 09:45:57 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2015-03-21 09:45:57 +0100 |
| commit | 58521e6066974833bb83e98a6bb17feb0c1fee90 (patch) | |
| tree | 1352e5073bc39e163c176f65c4dc310b677c20eb /plugins/extraction/haskell.ml | |
| parent | 364ea0c9d57df647af4f207d69eee002b2f8073e (diff) | |
Do not revert parameter lists when extracting singleton types to Haskell. (Fix for bugs #3470 and #3694)
Diffstat (limited to 'plugins/extraction/haskell.ml')
| -rw-r--r-- | plugins/extraction/haskell.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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))) |