Improve type inference and add `.` macro.

For tuples and `.` macro to work, type inference needed to be improved.
This improvement is to annotate metavars so they can't accidentally
refer to local vars.  IOW rather than "grafted", they're now "logical".
This also refined slightly the inversion of substitutions, tho I'm not sure
it makes an actual difference in the end.

* btl/pervasive.typer (BoolMod): Prototype of a Bool module.
(Pair): New type.
(__.__): New macro.

* emacs/typer-mode.el (typer-smie-rules): Add dangling `in` rule, as
used in OCaml.  Don't move up to the parent when indenting a `case` or
`lambda` with a `case`'s branch.

* src/debruijn.ml (scope_level, lctx_length): New types.
(elab_context): Add scope data.
(make_elab_context): Rename to empty_elab_context.
(ectx_new_scope, ectx_get_scope): New functions.

* src/debug_util.ml (main.ctx_to_cctx): Remove, use ectx_to_lctx instead.

* src/inverse_subst.ml (dummy_var): Remove.
(substIR): Add destination count.
(transfo.transfo): Refine the transformation so it is reversible.
(inverse): Check success.

* src/lexp.ml (lexp_name): Move so we can use lexp_string for
"trivial" cases.
(subst_string): Use it to avoid pathological cases.

* src/lparse.ml (_global_lexp_ctx): Remove.
(check): Shift metavars so they can't refer to vars from within the scope.
(infer_call.handle_fun_args): Unify two branches.
(lexp_decls_1, sform_letin): Introduce new scope for metavars.

* src/pexp.ml (pexp_p_actual_arg): Remove, unused.
(pexp_p_decls): Use sexp_u_list.

* tests/eval_test.ml: Add test of the `.` notation.