From fe99f87492c84530f76d1264b6888eefac3b60d1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 25 Jul 2016 15:46:24 +0200
Subject: [PATCH] Move tac_exist from classes to coq_tactics where it belongs.

---
 proofmode/classes.v     | 4 ----
 proofmode/coq_tactics.v | 4 ++++
 2 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/proofmode/classes.v b/proofmode/classes.v
index b84436e8e..a88e3daf7 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -301,10 +301,6 @@ Global Arguments from_exist {_} _ _ {_}.
 Global Instance from_exist_exist {A} (Φ: A → uPred M): FromExist (∃ a, Φ a) Φ.
 Proof. done. Qed.
 
-Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
-  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
-Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
-
 Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
   into_exist : P ⊢ ∃ x, Φ x.
 Global Arguments into_exist {_} _ _ {_}.
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 311a4d0ce..1ac516bbd 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -719,6 +719,10 @@ Lemma tac_forall_revert {A} Δ (Φ : A → uPred M) :
 Proof. intros HΔ a. by rewrite HΔ (forall_elim a). Qed.
 
 (** * Existential *)
+Lemma tac_exist {A} Δ P (Φ : A → uPred M) :
+  FromExist P Φ → (∃ a, Δ ⊢ Φ a) → Δ ⊢ P.
+Proof. intros ? [a ?]. rewrite -(from_exist P). eauto using exist_intro'. Qed.
+
 Lemma tac_exist_destruct {A} Δ i p j P (Φ : A → uPred M) Q :
   envs_lookup i Δ = Some (p, P) → IntoExist P Φ →
   (∀ a, ∃ Δ',
-- 
GitLab