• Dan Frumin's avatar
    Rewrite the rel_rec_r tactic to pick up the correct reduct · e13439ec
    Dan Frumin authored
    We have to call tac_rel_rec_r in reshape_expr because reshape_expr
    just decomposes the expression into a `(K',e')` without guaranteeing
    that `e` is actually head-reducible. Because of that it might be the
    case that `e` is `K[App (Rec f x e1) e2]`, but `e2` is not a value.
rel_tactics.v 15.8 KB