Commit 7a41c8ae authored by Dan Frumin's avatar Dan Frumin

Get rid of the unnecessary `iNext`

parent ddd905dc
......@@ -144,7 +144,7 @@ Tactic Notation "rel_pure_r" open_constr(ef) :=
|try (exact I || reflexivity || tac_rel_done) (* φ *)
|solve_ndisj (* specN E1 *)
|simpl; reflexivity (* eres = fill K e2 *)
|try iNext; simpl_subst/= (* new goal *)])
|simpl_subst/= (* new goal *)])
|| fail "rel_pure_r: cannot find the reduct".
Tactic Notation "rel_rec_r" := rel_pure_r (App (Rec _ _ _) _) || rel_pure_r (App _ _).
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment