Commit 261d7c64 authored by Robbert Krebbers's avatar Robbert Krebbers

Revert "Hack to delay type class inference in iPoseProof."

This reverts commit c43eb936.

The hack using class_apply has some strange behaviors, see:

  https://sympa.inria.fr/sympa/arc/coq-club/2016-07/msg00094.html
parent c43eb936
......@@ -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) :=
......
......@@ -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.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment