aboutsummaryrefslogtreecommitdiff
path: root/contrib/extraction/ocaml.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/ocaml.ml')
-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 ++