diff options
-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))) |