Fix various typing and inference problems with `Case`

* GNUmakefile (OBFLAGS): Add debug info.

* src/elexp.ml (elexp): Add binding of scrutinee in the default branch.
(elexp_string.maybe_str): Adjust print code accordingly.

* src/eval.ml (eval_case): Bind scrutinee in the default branch.

* src/lexp.ml (lexp): Add binding of scrutinee in the default branch.
(push_susp, _lexp_to_str): Adjust accordingly.
(lexp_unparse): Adjust to pexp changes.

* src/lparse.ml (elab_check_proper_type): Use lexp_print to get db indexes.
(ctx_extend): New function.
(_lexp_p_infer): Check that arrow's args are types.
(lexp_case): Rewrite; fix problems with scoping.
(lexp_read_pattern, lexp_read_pattern_args): Remove.

* src/opslexp.ml (lexp_whnf): Adjust to new `Case`.
Preserve the non-whnf in the sub-parts we return.
(check): Check that erasable inductive type fields have a proper type.
Don't assume call_split returns whnf elements.
Adjust to new `Case`.
(clean_maybe): Adjust to new `Case`.

* src/pexp.ml (ppat): Rename Ppatvar to Ppatsym since it can be either
a var or a constructor.  Drop arg_kind from Ppatcons.
(pexp_p_pat_arg): Only recognize := as explicit-implicit.
(pexp_u_pat_arg): Only use := for explicit-implicit.