From 261d7c644ea5dfecd66f72c257c22bc8507c0c0e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 27 Jul 2016 10:59:33 +0200
Subject: [PATCH] Revert "Hack to delay type class inference in iPoseProof."

This reverts commit c43eb936568049de062feb16bbf03915a4733e94.

The hack using class_apply has some strange behaviors, see:

  https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00094.html
---
 proofmode/tactics.v | 12 +++---------
 tests/proofmode.v   | 14 --------------
 2 files changed, 3 insertions(+), 23 deletions(-)

diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index ae3bd6443..3901386c4 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -208,11 +208,6 @@ Tactic Notation "iSpecialize" open_constr(t) :=
   end.
 
 (** * Pose proof *)
-(* We use [class_apply] in the below to delay type class inference, this is
-useful when difference [inG] instances are arround. See [tests/proofmode] for
-a simple but artificial example.
-
-Note that this only works when the posed lemma is prefixed with an [@]. *)
 Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
   lazymatch type of H1 with
   | string =>
@@ -221,10 +216,9 @@ Local Tactic Notation "iPoseProofCore" open_constr(H1) "as" constr(H2) :=
        |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
   | _ =>
      eapply tac_pose_proof with _ H2 _ _ _; (* (j:=H) *)
-       [first [class_apply H1|class_apply uPred.equiv_iff; eapply H1]
-       |(* [apply _] invokes TC inference on shelved goals, why ...? *)
-        typeclasses eauto
-       |env_cbv; class_apply eq_refl || fail "iPoseProof:" H2 "not fresh"|]
+       [first [eapply H1|apply uPred.equiv_iff; eapply H1]
+       |apply _
+       |env_cbv; reflexivity || fail "iPoseProof:" H2 "not fresh"|]
   end.
 
 Tactic Notation "iPoseProof" open_constr(t) "as" constr(H) :=
diff --git a/tests/proofmode.v b/tests/proofmode.v
index d1480fb13..7ac9b8956 100644
--- a/tests/proofmode.v
+++ b/tests/proofmode.v
@@ -106,17 +106,3 @@ Section iris.
     - done.
   Qed.
 End iris.
-
-Section classes.
-  Class C A := c : A.
-  Instance nat_C : C nat := 0.
-  Instance bool_C : C bool := true.
-
-  Lemma demo_9 {M : ucmraT} (P : uPred M)
-    (H : ∀ `{C A}, True ⊢ (c = c : uPred M)) : P ⊢ (c:nat) = c ∧ (c:bool) = c.
-  Proof.
-    iIntros "_".
-    iPoseProof (@H _) as "foo_bool". iPoseProof (@H _) as "foo_nat".
-    iSplit. iApply "foo_nat". iApply "foo_bool".
-  Qed.
-End classes.
-- 
GitLab