diff --git a/theories/tactics.v b/theories/tactics.v
index 88b809b0b947d060ae64d2eaacd8b1e4c54262be..507e582a107ef8e670a6777b9cfcdd2407aa8d8b 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. *)