Commit 11678073 authored by Robbert Krebbers's avatar Robbert Krebbers

Tweak some names in test file.

parent e4347ec2
Pipeline #31740 passed with stage
in 17 minutes and 5 seconds
...@@ -659,14 +659,14 @@ Tactic failure: iLöb: no 'BiLöb' instance found. ...@@ -659,14 +659,14 @@ Tactic failure: iLöb: no 'BiLöb' instance found.
1 subgoal 1 subgoal
PROP : bi PROP : bi
P1 : PROP P : PROP
P2, P3 : Prop φ1, φ2 : Prop
Himpl : P2 → P3 Himpl : φ1 → φ2
HP2 : P2 HP2 : φ1
============================ ============================
"HP" : P1 "HP" : P
--------------------------------------∗ --------------------------------------∗
P1 ∗ ⌜P3 P ∗ ⌜φ2
"test_not_fresh" "test_not_fresh"
: string : string
......
...@@ -1245,8 +1245,8 @@ Ltac ltac_tactics.string_to_ident_hook ::= ...@@ -1245,8 +1245,8 @@ Ltac ltac_tactics.string_to_ident_hook ::=
end). end).
Check "test_pure_name". Check "test_pure_name".
Lemma test_pure_name P1 (P2 P3: Prop) (Himpl: P2 -> P3) : Lemma test_pure_name P (φ1 φ2 : Prop) (Himpl : φ1 φ2) :
P1 P2 - P1 P3. P ⌜φ1 - P ⌜φ2.
Proof. Proof.
iIntros "[HP %HP2]". iIntros "[HP %HP2]".
Show. Show.
...@@ -1260,8 +1260,8 @@ Lemma test_iIntros_forall_pure_named (Ψ: nat → PROP) : ...@@ -1260,8 +1260,8 @@ Lemma test_iIntros_forall_pure_named (Ψ: nat → PROP) :
Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed. Proof. iIntros "HP". iIntros "%y". iApply ("HP" $! y). Qed.
Check "test_not_fresh". Check "test_not_fresh".
Lemma test_not_fresh P1 (P2: Prop) (H:P2) : Lemma test_not_fresh P (φ : Prop) (H : φ) :
P1 P2 - P1 P2. P φ - P φ .
Proof. Proof.
Fail iIntros "[H %H]". Fail iIntros "[H %H]".
Abort. Abort.
......
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