Get rid of unused `it` field in Case; various extra type checks
* src/lparse.ml (_lexp_p_check): Check the lambda's type annotations are indeed types. (lexp_case): Check that the subject is indeed of inductive type. (lexp_call): Remove unused `from_lctx`. (lexp_read_pattern): Remove unused `exp` arg. * src/lexp.ml (lexp): Remove unused "base inductive type" field from `Case`.
Loading
Please register or sign in to comment