Commit 9d39a93e authored by Ralf Jung's avatar Ralf Jung

Merge branch 'master+consequence-coq-pr9214-printing-bug-fixed' into 'master'

A Coq bug printing spurious parentheses has been fixed.

See merge request FP/iris-coq!197
parents 5b7f345c ec3eb238
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w (reverse xs ++ ys) -∗ Φ w
--------------------------------------∗
WP rev hd acc [{ v, Φ v }]
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
acc : val
ys : list val
Φ : val → iPropI Σ
============================
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w ys -∗ Φ w
--------------------------------------∗
WP match: InjLV #() with
InjL <> => acc
| InjR "l" =>
let: "tmp1" := Fst ! "l" in
let: "tmp2" := Snd ! "l" in
"l" <- ("tmp1", acc);; rev "tmp2" (InjLV #())
end [{ v, Φ v }]
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