aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-21 09:45:57 +0100
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-03-21 09:45:57 +0100
commit58521e6066974833bb83e98a6bb17feb0c1fee90 (patch)
tree1352e5073bc39e163c176f65c4dc310b677c20eb
parent364ea0c9d57df647af4f207d69eee002b2f8073e (diff)
Do not revert parameter lists when extracting singleton types to Haskell. (Fix for bugs #3470 and #3694)
-rw-r--r--plugins/extraction/haskell.ml6
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)))