Commit 19671d2f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Test case.

parent b4964be9
......@@ -633,6 +633,20 @@ k is used in hypothesis Hk.
: string
The command has indeed failed with message:
Tactic failure: iRevert: k is used in hypothesis "Hk".
"iNext_wrong_index"
: string
The command has indeed failed with message:
Tactic failure: iModIntro: cannot find modality
(modality_instances.modality_laterN (S i)) with pattern _.
"iModIntro_no_modality"
: string
The command has indeed failed with message:
Tactic failure: iModIntro: cannot find modality _ with pattern _.
"iNext_wrong_index"
: string
The command has indeed failed with message:
Tactic failure: iModIntro: cannot find modality _ with pattern
(□ _)%I.
"iLöb_no_BiLöb"
: string
The command has indeed failed with message:
......
......@@ -1142,6 +1142,18 @@ Proof. intros Hk. Fail iRevert (k). Abort.
Check "iRevert_dep_var".
Lemma iRevert_dep_var (k : nat) (Φ : nat PROP) : Φ k - Φ (S k).
Proof. iIntros "Hk". Fail iRevert (k). Abort.
Check "iNext_wrong_index".
Lemma iNext_wrong_index i P : P - ^i P.
Proof. iIntros "H". Fail iNext (S i). Abort.
Check "iModIntro_no_modality".
Lemma iModIntro_no_modality P : P - P.
Proof. iIntros "H". Fail iModIntro. Abort.
Check "iNext_wrong_index".
Lemma iModIntro_wrong_pattern P : P - P.
Proof. iIntros "H". Fail iModIntro ( _)%I. Abort.
End error_tests.
Section error_tests_bi.
......
Supports Markdown
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