Use sexps rather than pdecls
* src/lexp.ml (lexp_unparse.sdecls): Skip pexp_u_decls. * src/elab.ml (instantiate_implicit): Use Eval.varname. (lexp_decls_macro): Don't return a new context any more. Return a sexp rather than a list of pdecls. (lexp_check_decls): Take a list of sexps rather than a list of pdecls. Simplify the macro call case since it can't return a new ctx any more. (lexp_p_decls): Take a list of sexps rather than a list of pdecls. (sform_letin, default_ectx.read_file, _lexp_decl_str): Pass the sexps directly to lexp_p_decls. * src/debug_util.ml (format_source): Pass the sexps directly to lexp_p_decls. (mdecl, lexp_detect_recursive): Remove rather than fix. (main): Remove "pexp" debugging because there's no pexp any more. Remove "merge-debug" debugging because it's broken and it's not clear how to fix it. Pass the sexps directly to lexp_p_decls. * src/debug.ml (debug_pexp_decls): Remove; there's no pexp to debug any more. (debug_pexp_print_all): Remove unused. * src/REPL.ml (ipexp_parse): Use sexp rather then pdecl. (_raw_eval): Pass the sexps directly to lexp_p_decls. * src/pexp.ml (pdecl, pexp_p_decls, pexp_u_decl, pexp_u_decls) (pexp_decls_all, _pexp_decl_str, pexp_decl_str): Remove.
Loading
Please register or sign in to comment