diff --git a/tests/proofmode.ref b/tests/proofmode.ref index e45044a8275bdffdd30a5d1326d2afff652df913..39b74036b99d746399f31d1798e22f173965a949 100644 --- a/tests/proofmode.ref +++ b/tests/proofmode.ref @@ -515,8 +515,7 @@ Tactic failure: iExact: "HQ" not found. The command has indeed failed with message: Tactic failure: iExact: "HQ" : Q does not match goal. The command has indeed failed with message: -Tactic failure: iExact: "HP" -not absorbing and the remaining hypotheses not affine. +Tactic failure: iExact: remaining hypotheses not affine and the goal not absorbing. "iClear_fail" : string The command has indeed failed with message: @@ -581,13 +580,15 @@ Tactic failure: iApply: cannot apply P. "iApply_fail_not_affine_1" : string The command has indeed failed with message: -Tactic failure: iApply: Q -not absorbing and the remaining hypotheses not affine. +Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing. "iApply_fail_not_affine_2" : string The command has indeed failed with message: -Tactic failure: iApply: Q -not absorbing and the remaining hypotheses not affine. +Tactic failure: iApply: remaining hypotheses not affine and the goal not absorbing. +"iAssumption_fail_not_affine_1" + : string +The command has indeed failed with message: +Tactic failure: iAssumption: remaining hypotheses not affine and the goal not absorbing. "iRevert_wrong_var" : string The command has indeed failed with message: diff --git a/tests/proofmode.v b/tests/proofmode.v index e1c4ad8130edbb6d8f0ca792cb4b73ff0cf7d483..cd48f81ee2b19d072ff5238eb0ca4ce8282e55fc 100644 --- a/tests/proofmode.v +++ b/tests/proofmode.v @@ -1018,9 +1018,13 @@ Lemma iApply_fail_not_affine_1 P Q : P -∗ Q -∗ Q. Proof. iIntros "HP HQ". Fail iApply "HQ". Abort. Check "iApply_fail_not_affine_2". -Lemma iApply_fail_not_affine_1 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q. +Lemma iApply_fail_not_affine_2 P Q R : P -∗ R -∗ (R -∗ Q) -∗ Q. Proof. iIntros "HP HR HQ". Fail iApply ("HQ" with "HR"). Abort. +Check "iAssumption_fail_not_affine_1". +Lemma iAssumption_fail_not_affine_1 P Q : P -∗ Q -∗ Q. +Proof. iIntros "HP HQ". Fail iAssumption. Abort. + Check "iRevert_wrong_var". Lemma iRevert_wrong_var (k : nat) (Φ : nat → PROP) : ⊢ Φ (S k). Proof. diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v index 418f25c0db18669065a873a724773286758e2099..550ec120987723784b93d1034711aaace608182f 100644 --- a/theories/proofmode/ltac_tactics.v +++ b/theories/proofmode/ltac_tactics.v @@ -243,7 +243,7 @@ Tactic Notation "iExact" constr(H) := fail "iExact:" H ":" P "does not match goal" |pm_reduce; iSolveTC || let H := pretty_ident H in - fail "iExact:" H "not absorbing and the remaining hypotheses not affine"]. + fail "iExact: remaining hypotheses not affine and the goal not absorbing"]. Tactic Notation "iAssumptionCore" := let rec find Γ i P := @@ -269,9 +269,9 @@ Tactic Notation "iAssumption" := [pose proof (_ : FromAssumption p P Q) as Hass; eapply (tac_assumption _ j p P); [pm_reflexivity - |apply Hass + |exact Hass |pm_reduce; iSolveTC || - fail 1 "iAssumption:" j "not absorbing and the remaining hypotheses not affine"] + fail 2 "iAssumption: remaining hypotheses not affine and the goal not absorbing"] |assert (P = False%I) as Hass by reflexivity; apply (tac_false_destruct _ j p P); [pm_reflexivity @@ -1142,7 +1142,7 @@ Local Ltac iApplyHypExact H := |pm_reduce; iSolveTC] |lazymatch iTypeOf H with | Some (_,?Q) => - fail 2 "iApply:" Q "not absorbing and the remaining hypotheses not affine" + fail 2 "iApply: remaining hypotheses not affine and the goal not absorbing" end]. Local Ltac iApplyHypLoop H := first