reparation des Extract Constant avec Haskell

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 7 deletions

diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index d00e36f60c..3797e5d97c 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -66,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt ()
 
 let fnl2 () = fnl () ++ fnl () 
 
+let pp_parameters l = 
+  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+
+let pp_string_parameters l = 
+  (pp_boxed_tuple str l ++ space_if (l<>[])) 
+
 (*s Generic renaming issues. *)
 
 let rec rename_id id avoid = 
@@ -184,7 +190,6 @@ 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)
 
@@ -385,12 +390,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
 	
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_parameters l = 
-  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
-
-let pp_string_parameters l = 
-  (pp_boxed_tuple str l ++ space_if (l<>[])) 
-
 let pp_one_ind prefix ip pl cv =
   let pl = rename_tvars keywords pl in
   let pp_constructor (r,l) =