Also apply generalization to inductive type constructors
* src/elab.ml (generalize): Change calling convention. (infer_and_generalize_type, infer_and_generalize_def): Adjust accordingly. (lexp_parse_inductive.make_args): Generalize constructors. (var_of_ovar): Move to lexp.ml. * src/opslexp.ml (check', get_type): Fix scoping of `level` in Inductive. * btl/builtins.typer (Eq_comm): Take advantage of improvements in gneralization and unification. * btl/pervasive.typer (BoolMod): Avoid `typecons`'s generalizing. (LList): New type, to test typecons's generalization. * src/lexp.ml (var_of_ovar): Move from elab.ml. (lexp_unparse): Simplify. * src/pexp.ml (pexp_u_ind_arg): Remove.
Loading
Please register or sign in to comment