Commit 330702cc authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Improve name generation in the injection' tactic.

The tactic "injection' H" now uses the name "H" for the first hypothesis it
generates. Fresh names will still be used for the remaining hypotheses.
parent 5a73c4ed
...@@ -115,7 +115,8 @@ Ltac unblock_hyps := unfold block in * |-. ...@@ -115,7 +115,8 @@ Ltac unblock_hyps := unfold block in * |-.
(** The tactic [injection' H] is a variant of injection that introduces the (** The tactic [injection' H] is a variant of injection that introduces the
generated equalities. *) generated equalities. *)
Ltac injection' H := block_goal; injection H; clear H; intros; unblock_goal. Ltac injection' H :=
block_goal; injection H; clear H; intros H; intros; unblock_goal.
(** The tactic [simplify_equality] repeatedly substitutes, discriminates, (** The tactic [simplify_equality] repeatedly substitutes, discriminates,
and injects equalities, and tries to contradict impossible inequalities. *) and injects equalities, and tries to contradict impossible inequalities. *)
......
Supports Markdown
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