aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/declaremods.ml
diff options
context:
space:
mode:
authorGravatar Nickolai Zeldovich <nickolai@csail.mit.edu>2016-02-08 16:08:10 -0500
committerGravatar Nickolai Zeldovich <nickolai@csail.mit.edu>2016-02-19 16:02:30 -0500
commit8bac7b9e0a149cd8f374ac63f33ec4ecfc5ae2d2 (patch)
tree8a1617989f89e2c20b688b2be00b9423220587de /library/declaremods.ml
parenta4b457bef4290fed3f2869795f1539de53b3805a (diff)
Fix Haskell extraction for terms over 45 characters long
The Haskell extraction code would allow line-wrapping of the Haskell type definition, which would lead to unparseable Haskell code when the linebreak occured just before the type name. In particular, with a term name of 46 characters or more, the following Coq code: Definition xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx := tt. Extraction Language Haskell. Extraction xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx. would produce: xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx :: Unit xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx = Tt which failed to compile with GHC (according to Haskell's indentation rules, the "Unit" line must be indented to be treated as a continuation of the previous line). This patch always forces the type onto a separate line, and ensures that it is always indented by 2 spaces (just like the body of each definition).
Diffstat (limited to 'library/declaremods.ml')
0 files changed, 0 insertions, 0 deletions