Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
Pierre-Marie Pédrot
Iris
Commits
ec3eb238
Commit
ec3eb238
authored
Dec 16, 2018
by
Hugo Herbelin
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
A Coq bug printing spurious parentheses has been fixed.
See Coq PR#9214.
parent
b85a3cfc
Changes
1
Hide whitespace changes
Inline
Side-by-side
Showing
1 changed file
with
33 additions
and
0 deletions
+33
-0
tests/list_reverse.8.10.ref
tests/list_reverse.8.10.ref
+33
-0
No files found.
tests/list_reverse.8.10.ref
0 → 100644
View file @
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 }]
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment