From 330702cccfb25690b5157a2d0b775759012ae16a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 8 Feb 2015 18:11:23 +0100
Subject: [PATCH] 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.
---
 theories/tactics.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/tactics.v b/theories/tactics.v
index 88b809b0..507e582a 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -115,7 +115,8 @@ Ltac unblock_hyps := unfold block in * |-.
 
 (** The tactic [injection' H] is a variant of injection that introduces the
 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,
 and injects equalities, and tries to contradict impossible inequalities. *)
-- 
GitLab