aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/haskell.ml
diff options
context:
space:
mode:
authorletouzey2002-12-05 14:43:14 +0000
committerletouzey2002-12-05 14:43:14 +0000
commitb86f8d977d9a0dd9635207e436bc1e59ca98475c (patch)
tree5c630a49ea16802fe3f60c1686e8080694a90338 /contrib/extraction/haskell.ml
parentf4af459e05814c954514f71dcc4c63b00af823b5 (diff)
code cleanup (+ debut de commencement de modules)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/haskell.ml')
-rw-r--r--contrib/extraction/haskell.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 07e6fdbe2f..149b9967cb 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -14,12 +14,9 @@ open Pp
open Util
open Names
open Nameops
-open Term
open Miniml
open Mlutil
-open Options
open Ocaml
-open Nametab
(*s Haskell renaming issues. *)
@@ -75,6 +72,7 @@ let rec pp_type par vl t =
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
| Tdummy -> str "()"
| Tunknown -> str "()"
+ | Tcustom s -> str s
in
hov 0 (pp_rec par t)
@@ -140,6 +138,7 @@ let rec pp_expr par env args =
str "__" (* An [MLdummy] may be applied, but I don't really care. *)
| MLcast (a,t) -> pp_expr par env args a
| MLmagic a -> pp_expr par env args a
+ | MLcustom s -> str s
and pp_pat env pv =
let pp_one_pat (name,ids,t) =