From 8e636f205f38c7891bb2f6416d8ea710762c2df3 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 17 Feb 2016 15:47:49 +0100
Subject: [PATCH] Remove injection' tactic.
The tactic injection H as H is doing exactly that.
---
heap_lang/tactics.v | 2 +-
prelude/tactics.v | 34 ++++++++--------------------------
2 files changed, 9 insertions(+), 27 deletions(-)
diff --git a/heap_lang/tactics.v b/heap_lang/tactics.v
index b55375ed8..f85d34ceb 100644
--- a/heap_lang/tactics.v
+++ b/heap_lang/tactics.v
@@ -16,7 +16,7 @@ Ltac inv_step :=
| H : prim_step _ _ _ _ _ |- _ => destruct H; subst
| H : _ = fill ?K ?e |- _ =>
destruct K as [|[]];
- simpl in H; first [subst e|discriminate H|injection' H]
+ simpl in H; first [subst e|discriminate H|injection H as H]
(* ensure that we make progress for each subgoal *)
| H : head_step ?e _ _ _ _, Hv : of_val ?v = fill ?K ?e |- _ =>
apply values_head_stuck, (fill_not_val K) in H;
diff --git a/prelude/tactics.v b/prelude/tactics.v
index 665b96f63..9381626a9 100644
--- a/prelude/tactics.v
+++ b/prelude/tactics.v
@@ -117,25 +117,6 @@ does the converse. *)
Ltac var_eq x1 x2 := match x1 with x2 => idtac | _ => fail 1 end.
Ltac var_neq x1 x2 := match x1 with x2 => fail 1 | _ => idtac end.
-(** The tactics [block_hyps] and [unblock_hyps] can be used to temporarily mark
-certain hypothesis as being blocked. The tactic changes all hypothesis [H: T]
-into [H: blocked T], where [blocked] is the identity function. If a hypothesis
-is already blocked, it will not be blocked again. The tactic [unblock_hyps]
-removes [blocked] everywhere. *)
-
-Ltac block_hyp H :=
- lazymatch type of H with
- | block _ => idtac | ?T => change T with (block T) in H
- end.
-Ltac block_hyps := repeat_on_hyps (fun H =>
- match type of H with block _ => idtac | ?T => change (block T) in H end).
-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 H; intros; unblock_goal.
-
(** The tactic [simplify_equality] repeatedly substitutes, discriminates,
and injects equalities, and tries to contradict impossible inequalities. *)
Ltac fold_classes :=
@@ -189,13 +170,14 @@ Ltac simplify_equality := repeat
| H : _ = _ |- _ => discriminate H
| H : ?f _ = ?f _ |- _ => apply (inj f) in H
| H : ?f _ _ = ?f _ _ |- _ => apply (inj2 f) in H; destruct H
- (* before [injection'] to circumvent bug #2939 in some situations *)
- | H : ?f _ = ?f _ |- _ => injection' H
- | H : ?f _ _ = ?f _ _ |- _ => injection' H
- | H : ?f _ _ _ = ?f _ _ _ |- _ => injection' H
- | H : ?f _ _ _ _ = ?f _ _ _ _ |- _ => injection' H
- | H : ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _ => injection' H
- | H : ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _ => injection' H
+ (* before [injection] to circumvent bug #2939 in some situations *)
+ | H : ?f _ = ?f _ |- _ => injection H as H
+ (* first hyp will be named [H], subsequent hyps will be given fresh names *)
+ | H : ?f _ _ = ?f _ _ |- _ => injection H as H
+ | H : ?f _ _ _ = ?f _ _ _ |- _ => injection H as H
+ | H : ?f _ _ _ _ = ?f _ _ _ _ |- _ => injection H as H
+ | H : ?f _ _ _ _ _ = ?f _ _ _ _ _ |- _ => injection H as H
+ | H : ?f _ _ _ _ _ _ = ?f _ _ _ _ _ _ |- _ => injection H as H
| H : ?x = ?x |- _ => clear H
(* unclear how to generalize the below *)
| H1 : ?o = Some ?x, H2 : ?o = Some ?y |- _ =>
--
GitLab