Commit 1e00275c authored by Robbert Krebbers's avatar Robbert Krebbers

Fix errors of `iAssumption`, `iExact`, and friends.

- The error messages were wrong: the goal needs to be absorbing, not the hypothesis.
- The wrong failure number was used in `iAssumption`, which caused the error not
  to be propagated properly.
parent a7b4c684
......@@ -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:
......
......@@ -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.
......
......@@ -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
......
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