diff options
author | 2004-09-06 07:49:51 +0000 | |
---|---|---|
committer | 2004-09-06 07:49:51 +0000 | |
commit | cc746ea32b1dd61dff9c82db68f2f8ef2131af3f (patch) | |
tree | 8d60faf1a917b330d0e0fa898a7eb6db33cde21d /contrib/extraction/ocaml.ml | |
parent | 4580470c8fe002c0077d96abaf32f180ee5c7455 (diff) |
reparation des Extract Constant avec Haskell
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6064 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/ocaml.ml')
-rw-r--r-- | contrib/extraction/ocaml.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index d00e36f60..3797e5d97 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) = |