* src/lparse.ml (_lexp_decls): Rewrite to fix scoping issues
* src/lparse.ml (elab_check_sort, elab_check_proper_type): New functions. (elab_check_def, ctx_define_rec._): Use them to check that the types are proper types. (lexp_detect_recursive, _lexp_rec_decl): Remove. (lexp_check_decls, lexp_decls_1): New functions. (_lexp_decls): Use them instead. * src/opslexp.ml (check) <Arrow>: Fix incorrect context for target. * src/util.ml (IntMap): New module. * src/debug_util.ml (lexp_detect_recursive): Move from lparse.ml.
Loading
Please register or sign in to comment