Extraction: improved indentation of extracted code (fix #2497)

 For Haskell, we still try to provide readable indentation,
 but we now avoid relying on this indentation for correctness.
 Instead, we use layout-independant syntax with { } when
 necessary (after "case of" and "let"). It is much safer this
 way, even if the syntax gets a bit more cumbersome.

 For people allergic to {;}, they can most of the time do a
 tr -d "{;}" without changing the meaning of the program.
 Be careful nonetheless: since "case of" is now delimited,
 some parenthesis that used to be mandatory are now removed.

 Note also that the initial "module ... where" is still without
 { }: even when Format goes crazy it doesn't tamper with column 0.

 Other modifications:

 - Using "Set Printing Width" now affects uniformly the extraction
 pretty-printers. You can set a greater value than the default 78
 before extracting a program that you know to be "really deep".

 - In ocaml (and also a bit in Haskell), we now try to avoid abusing
 of 2-char-right-indentation. For instance | is now aligned with
 the "m" of match. This way, max_indent will be reached less frequently.

 - As soon as a pretty-print box contains an explicit newline,
 we set its virtual size to a big number, in order to prevent this
 box to be part of some horizontal arrangement.

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

1 files changed, 4 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 325490969..3a6863138 100644
--- a/CHANGES
+++ b/CHANGES
@@ -73,6 +73,10 @@ Internal infrastructure
 - Support of cross-compilation via mingw toward Windows, contact P. Letouzey
   for more informations.
 
+Extraction
+
+- The pretty-printer for Haskell now produces layout-independant code
+
 Changes from V8.2 to V8.3
 =========================