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
119f7f41
Commit
119f7f41
authored
Jan 19, 2019
by
Ralf Jung
Browse files
Options
Browse Files
Download
Plain Diff
Merge branch 'ralf/mod-pretty' into 'master'
prettify after iMod See merge request FP/iris-coq!201
parents
7de018e3
3a8a6fe7
Changes
4
Hide whitespace changes
Inline
Side-by-side
Showing
4 changed files
with
42 additions
and
2 deletions
+42
-2
Makefile.coq.local
Makefile.coq.local
+1
-1
tests/atomic.ref
tests/atomic.ref
+31
-0
tests/atomic.v
tests/atomic.v
+9
-0
theories/proofmode/ltac_tactics.v
theories/proofmode/ltac_tactics.v
+1
-1
No files found.
Makefile.coq.local
View file @
119f7f41
...
...
@@ -8,7 +8,7 @@ test: $(TESTFILES:.v=.vo)
.PHONY
:
test
COQ_TEST
=
$(COQTOP)
$(COQDEBUG)
-batch
-test-mode
COQ_BROKEN
=
$(
shell
echo
"
$(COQ_VERSION)
"
| egrep
"^8
\.
10
\b
"
>
/dev/null
&&
echo
1
)
COQ_BROKEN
=
$(
shell
echo
"
$(COQ_VERSION)
"
| egrep
"^8
\.
(9|
10
)
\b
"
>
/dev/null
&&
echo
1
)
# Can't use pipes because that discards error codes and dash provides no way to control that.
# Also egrep errors if it doesn't match anything, we have to ignore that.
...
...
tests/atomic.ref
View file @
119f7f41
...
...
@@ -338,3 +338,34 @@
--------------------------------------∗
WP code {{ v, Φ v }}
"Prettification"
: string
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
============================
--------------------------------------∗
∀ Φ : language.val heap_lang → iProp Σ, AU << ∀
x : val,
P x >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>
-∗ WP ! #0 {{ v, Φ v }}
1 subgoal
Σ : gFunctors
heapG0 : heapG Σ
P : val → iProp Σ
Φ : language.val heap_lang → iProp Σ
============================
"AU" : ∃ x : val, P x
∗ (P x
={∅,⊤}=∗ AU << ∀ x0 : val,
P x0 >> @ ⊤, ∅
<< ∃ y : val, P y, COMM Φ #() >>)
∧ (∀ x0 : val, P x0 ={∅,⊤}=∗ Φ #())
--------------------------------------∗
WP ! #0 @ ∅ {{ v, |={∅,⊤}=> Φ v }}
tests/atomic.v
View file @
119f7f41
...
...
@@ -88,4 +88,13 @@ Section printing.
Show
.
iIntros
(
Q
Φ
)
"? AU"
.
Show
.
Abort
.
Check
"Prettification"
.
Lemma
iMod_prettify
(
P
:
val
→
iProp
Σ
)
:
<<<
∀
x
,
P
x
>>>
!#
0
@
⊤
<<<
∃
y
,
P
y
,
RET
#()
>>>.
Proof
.
iApply
wp_atomic_intro
.
Show
.
iIntros
(
Φ
)
"AU"
.
iMod
"AU"
.
Show
.
Abort
.
End
printing
.
theories/proofmode/ltac_tactics.v
View file @
119f7f41
...
...
@@ -1214,7 +1214,7 @@ Tactic Notation "iModCore" constr(H) :=
fail
"iMod: cannot eliminate modality"
P
"in"
Q
|
iSolveSideCondition
|
pm_reflexivity
|
(* subgoal *)
].
|
pm_prettify
(* subgoal *)
].
(** * Basic destruct tactic *)
Local
Ltac
iDestructHypGo
Hz
pat
:
=
...
...
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