Skip to content
GitLab
Projects
Groups
Snippets
/
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Menu
Open sidebar
Iris
examples
Commits
2d6aa0bd
Commit
2d6aa0bd
authored
May 25, 2019
by
Ralf Jung
Browse files
logrel: fix for Coq master
parent
42d6747d
Pipeline
#16961
canceled with stage
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/logrel/F_mu/logrel.v
View file @
2d6aa0bd
...
...
@@ -88,7 +88,7 @@ Section logrel.
env_Persistent
Δ
→
Persistent
(
ctx_lookup
x
Δ
v
).
Proof
.
intros
H
Δ
;
revert
x
;
induction
H
Δ
=>-[|?]
/=
;
apply
_
.
Qed
.
Global
Instance
interp_persistent
τ
Δ
v
:
env_Persistent
Δ
→
Persistent
(
⟦
τ
⟧
Δ
v
)
:
=
_
.
env_Persistent
Δ
→
Persistent
(
⟦
τ
⟧
Δ
v
).
Proof
.
revert
v
Δ
;
induction
τ
=>
v
Δ
H
Δ
;
simpl
;
try
apply
_
.
rewrite
/
Persistent
fixpoint_interp_rec1_eq
/
interp_rec1
/=
intuitionistically_into_persistently
.
...
...
theories/logrel/F_mu_ref_conc/examples/lock.v
View file @
2d6aa0bd
...
...
@@ -159,7 +159,7 @@ Section proof.
Global
Opaque
with_lock
.
End
proof
.
Global
Hint
Rewrite
newlock_closed
:
autosubst
.
Global
Hint
Rewrite
acquire_closed
:
autosubst
.
Global
Hint
Rewrite
release_closed
:
autosubst
.
Global
Hint
Rewrite
with_lock_subst
:
autosubst
.
Hint
Rewrite
newlock_closed
:
autosubst
.
Hint
Rewrite
acquire_closed
:
autosubst
.
Hint
Rewrite
release_closed
:
autosubst
.
Hint
Rewrite
with_lock_subst
:
autosubst
.
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
View file @
2d6aa0bd
...
...
@@ -79,7 +79,7 @@ Section CG_Stack.
Lemma
CG_push_subst
(
st
:
expr
)
f
:
(
CG_push
st
).[
f
]
=
CG_push
st
.[
f
].
Proof
.
unfold
CG_push
;
asimpl
;
trivial
.
Qed
.
Global
Hint
Rewrite
CG_push_subst
:
autosubst
.
Hint
Rewrite
CG_push_subst
:
autosubst
.
Lemma
steps_CG_push
E
ρ
j
K
st
v
w
:
nclose
specN
⊆
E
→
...
...
@@ -451,13 +451,13 @@ Section CG_Stack.
End
CG_Stack
.
Global
Hint
Rewrite
CG_push_subst
:
autosubst
.
Global
Hint
Rewrite
CG_locked_push_subst
:
autosubst
.
Global
Hint
Rewrite
CG_locked_pop_subst
:
autosubst
.
Global
Hint
Rewrite
CG_pop_subst
:
autosubst
.
Global
Hint
Rewrite
CG_locked_pop_subst
:
autosubst
.
Global
Hint
Rewrite
CG_snap_subst
:
autosubst
.
Global
Hint
Rewrite
CG_iter_subst
:
autosubst
.
Global
Hint
Rewrite
CG_snap_iter_subst
:
autosubst
.
Global
Hint
Rewrite
CG_stack_body_subst
:
autosubst
.
Global
Hint
Rewrite
CG_stack_closed
:
autosubst
.
Hint
Rewrite
CG_push_subst
:
autosubst
.
Hint
Rewrite
CG_locked_push_subst
:
autosubst
.
Hint
Rewrite
CG_locked_pop_subst
:
autosubst
.
Hint
Rewrite
CG_pop_subst
:
autosubst
.
Hint
Rewrite
CG_locked_pop_subst
:
autosubst
.
Hint
Rewrite
CG_snap_subst
:
autosubst
.
Hint
Rewrite
CG_iter_subst
:
autosubst
.
Hint
Rewrite
CG_snap_iter_subst
:
autosubst
.
Hint
Rewrite
CG_stack_body_subst
:
autosubst
.
Hint
Rewrite
CG_stack_closed
:
autosubst
.
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
View file @
2d6aa0bd
...
...
@@ -329,9 +329,9 @@ Section FG_stack.
End
FG_stack
.
Global
Hint
Rewrite
FG_push_subst
:
autosubst
.
Global
Hint
Rewrite
FG_pop_subst
:
autosubst
.
Global
Hint
Rewrite
FG_iter_subst
:
autosubst
.
Global
Hint
Rewrite
FG_read_iter_subst
:
autosubst
.
Global
Hint
Rewrite
FG_stack_body_subst
:
autosubst
.
Global
Hint
Rewrite
FG_stack_closed
:
autosubst
.
Hint
Rewrite
FG_push_subst
:
autosubst
.
Hint
Rewrite
FG_pop_subst
:
autosubst
.
Hint
Rewrite
FG_iter_subst
:
autosubst
.
Hint
Rewrite
FG_read_iter_subst
:
autosubst
.
Hint
Rewrite
FG_stack_body_subst
:
autosubst
.
Hint
Rewrite
FG_stack_closed
:
autosubst
.
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new 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