aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2002-02-25 17:14:22 +0000
committerletouzey2002-02-25 17:14:22 +0000
commit01fa1f609e428cb63608850b4f99cffe9b833ce2 (patch)
treec6b6171acef21961aba25a1563cefac5421e9c54
parenteffd1a1d46db1f5d801b05c4aaeda89b7a735d9c (diff)
pretty print des Cases devenant des let-in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2494 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/extraction/ocaml.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index db64c1e727..42b7cbf9c3 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -167,6 +167,7 @@ let rec pp_type par ren t =
let expr_needs_par = function
| MLlam _ -> true
+ | MLcase (_,[|_|]) -> false
| MLcase _ -> true
| _ -> false