aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2002-11-29 00:29:26 +0000
committerletouzey2002-11-29 00:29:26 +0000
commit8f2719afe8699a6053cdf92294e171d72e373146 (patch)
treec767756ee792af00196f87757d50436943386fb3
parenta1c371517cba649142559cfe02a8de6a5938893e (diff)
cosmetique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3337 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/extraction/ocaml.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 582dbd2abc..55e53acfa2 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -412,7 +412,7 @@ let pp_decl = function
| Dterm (r, a, t) when is_proj r ->
let e = pp_global r in
(pp_val e t ++
- hov 0 (str "let " ++ e ++ str " x = x." ++ e ++ fnl() ++ fnl ()))
+ hov 0 (str "let " ++ e ++ str " x = x." ++ e ++ fnl()))
| Dterm (r, a, t) ->
let e = pp_global r in
(pp_val e t ++