From d7d23b5eea2b167efb75b6b29a8eaef46626425d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 5 Aug 2016 17:08:36 +0200
Subject: [PATCH] Remove duplicate iVs and iVsIntro tactic.

---
 proofmode/tactics.v | 13 -------------
 1 file changed, 13 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index 817c628a8..49e373371 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -874,19 +874,6 @@ Ltac iSimplifyEq := repeat (
   || simplify_eq/=).
 
 (** * View shifts *)
-Tactic Notation "iVsIntro" :=
-  eapply tac_vs_intro;
-    [let P := match goal with |- FromVs ?P _ => P end in
-     apply _ || fail "iVsIntro:" P "not a viewshift"|].
-
-Tactic Notation "iVsCore" constr(H) :=
-  eapply tac_vs_elim with _ H _ _ _ _;
-    [env_cbv; reflexivity || fail "iVs:" H "not found"
-    |let P := match goal with |- ElimVs ?P _ _ _ => P end in
-     let Q := match goal with |- ElimVs _ _ _ ?Q => Q end in
-     apply _ || fail "iVs: cannot eliminate" H ":" P "in" Q
-    |env_cbv; reflexivity|].
-
 Tactic Notation "iVs" open_constr(lem) :=
   iDestructCore lem as (fun H => iVsCore H; last iDestruct H as "?").
 Tactic Notation "iVs" open_constr(lem) "as" constr(pat) :=
-- 
GitLab