Generalize non-recursive let-definitions

* btl/pervasive.typer (List_head, List_tail, Sexp_to_list.singleton):
Let Typer generalize the definition's type.

* src/elab.ml (newMetalevel): Add a `loc` argument.
(generalize): New function, extracted from infer_and_generalize_type.
(track_fv): Adjust to new output of `OL.fv`.
(infer_and_generalize_type): Use `generalize`.
(infer_and_generalize_def): New function.
(lexp_decls_1): Use it for non-recursive definitions.

* src/eval.ml (closed_p): Adjust to new output of `OL.fv`.

* src/opslexp.ml (mv_set): Add info to keep track of erasability.
(mv_set_erase, fv_erase): New functions.
(fv): Use them.

* src/unification.ml (_unify_metavar.unif): Return None in case of
failure of inversion.