Fix some context and whnf handling in `check`.

* src/debruijn.ml (lctx_extend): Change vdef arg to be an option.

* src/lparse.ml (lexp_decls_1): Fix inf-loop on structural equality.
(elab_check_def): Add debug output.  Don't call conv_p.
(ctx_define_rec): Do check that it's properly typed.

* src/opslexp.ml (check) <Let>, <Lambda>, <Case>: Call lexp_whnf.
(check) <Inductive>: Fix context computation for fields.