Now that I'm not in a hurry to get a bugfix out, I thought I'd reflect at greater length on the question about let-generalization. An easily overlooked feature of Llama Light is that it is written in Llama Light. The fact that this substantial codebase can be written without let-generalization (and hardly any changes) supports the thesis of that paper and , in my opinion, further demonstrates that explicit polymorphism (which has its own complexities) is not even necessary to redeem anything. The most intrusive changes were to the following not-that-common idiom: "let raise_foo x y = raise (Foo (x, y)) in ..." which is then used in multiple, incompatible locations. The workaround is simply "let make_foo x y = Foo (x, y) in ..." which is then raised explicitly. I confess however that the "Scanf" module has not been ported due to a complex use of let-generalization which I have not yet managed to pull apart (anyone want to contribute? ;-). And yes, this is relevant to my (more theoretical) work (although I could certainly live with a system that had let-generalization). In particular HOL, higher-order logic, does not have it, and because of this, HOL can be interpreted in weak versions of set theory that are easily trusted. As for the location in the documentation, I'll consider changing it...but the basic idea was to write a page that would make sense for non-OCaml users. For comparison, the OCaml manual mentions *nowhere* that let *is* generalized :) Please keep the bug reports (and non-bug reports) coming! The toplevel bug was due to overzealous last-minute Makefile pruning...but that's no excuse, I ought to have a real testing system. Thanks, -Jeremy