diff --git a/proofmode/tactics.v b/proofmode/tactics.v index ae3bd64434ee3caeb80b7e741e09aabba91464eb..3901386c43ad909a114baeac44a5608ad5a6b1fd 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 d1480fb1391557730d23b7e282ccce47c05c74b1..7ac9b89561e967ad0703eb8cb86ee56e2c76f4f0 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.