Skip to content
GitLab
Menu
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
636f6fb3
Commit
636f6fb3
authored
Dec 11, 2018
by
Amin Timany
Browse files
Remove global from Typeclasses Opaque (not supported in Coq 8.7)
parent
21c3fd10
Pipeline
#13333
failed with stage
in 5 minutes and 59 seconds
Changes
4
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/logrel/F_mu_ref_conc/examples/fact.v
View file @
636f6fb3
...
...
@@ -49,7 +49,7 @@ Lemma fact_acc_body_unfold :
).
Proof
.
trivial
.
Qed
.
Global
Typeclasses
Opaque
fact_acc_body
.
Typeclasses
Opaque
fact_acc_body
.
Global
Opaque
fact_acc_body
.
Definition
fact_acc
:
expr
:
=
...
...
theories/logrel/F_mu_ref_conc/examples/lock.v
View file @
636f6fb3
...
...
@@ -35,7 +35,7 @@ Proof. trivial. Qed.
Lemma
with_lock_of_val
e
l
:
of_val
(
with_lockV
e
l
)
=
with_lock
e
l
.
Proof
.
trivial
.
Qed
.
Global
Typeclasses
Opaque
with_lockV
.
Typeclasses
Opaque
with_lockV
.
Global
Opaque
with_lockV
.
Lemma
newlock_closed
f
:
newlock
.[
f
]
=
newlock
.
...
...
@@ -93,7 +93,7 @@ Section proof.
by
iMod
(
step_alloc
_
_
j
K
with
"[Hj]"
)
as
"Hj"
;
eauto
.
Qed
.
Global
Typeclasses
Opaque
newlock
.
Typeclasses
Opaque
newlock
.
Global
Opaque
newlock
.
Lemma
steps_acquire
E
ρ
j
K
l
:
...
...
@@ -112,7 +112,7 @@ Section proof.
Unshelve
.
all
:
trivial
.
Qed
.
Global
Typeclasses
Opaque
acquire
.
Typeclasses
Opaque
acquire
.
Global
Opaque
acquire
.
Lemma
steps_release
E
ρ
j
K
l
b
:
...
...
@@ -126,7 +126,7 @@ Section proof.
by
iIntros
"!> {$Hj $Hl}"
.
Qed
.
Global
Typeclasses
Opaque
release
.
Typeclasses
Opaque
release
.
Global
Opaque
release
.
Lemma
steps_with_lock
E
ρ
j
K
e
l
P
Q
v
w
:
...
...
@@ -155,7 +155,7 @@ Section proof.
iModIntro
;
by
iFrame
.
Qed
.
Global
Typeclasses
Opaque
with_lock
.
Typeclasses
Opaque
with_lock
.
Global
Opaque
with_lock
.
End
proof
.
...
...
theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
View file @
636f6fb3
...
...
@@ -97,7 +97,7 @@ Section CG_Stack.
iModIntro
.
by
iFrame
.
Qed
.
Global
Typeclasses
Opaque
CG_push
.
Typeclasses
Opaque
CG_push
.
Global
Opaque
CG_push
.
Lemma
CG_locked_push_to_val
st
l
:
...
...
@@ -137,7 +137,7 @@ Section CG_Stack.
iApply
steps_CG_push
;
first
done
.
by
iFrame
.
Qed
.
Global
Typeclasses
Opaque
CG_locked_push
.
Typeclasses
Opaque
CG_locked_push
.
Global
Opaque
CG_locked_push
.
(* Coarse-grained pop *)
...
...
@@ -209,7 +209,7 @@ Section CG_Stack.
by
iFrame
"Hj Hx"
;
trivial
.
Qed
.
Global
Typeclasses
Opaque
CG_pop
.
Typeclasses
Opaque
CG_pop
.
Global
Opaque
CG_pop
.
Lemma
CG_locked_pop_to_val
st
l
:
...
...
@@ -265,7 +265,7 @@ Section CG_Stack.
iApply
steps_CG_pop_fail
;
eauto
.
Qed
.
Global
Typeclasses
Opaque
CG_locked_pop
.
Typeclasses
Opaque
CG_locked_pop
.
Global
Opaque
CG_locked_pop
.
Lemma
CG_snap_to_val
st
l
:
to_val
(
CG_snap
st
l
)
=
Some
(
CG_snapV
st
l
).
...
...
@@ -274,7 +274,7 @@ Section CG_Stack.
Lemma
CG_snap_of_val
st
l
:
of_val
(
CG_snapV
st
l
)
=
CG_snap
st
l
.
Proof
.
trivial
.
Qed
.
Global
Typeclasses
Opaque
CG_snapV
.
Typeclasses
Opaque
CG_snapV
.
Global
Opaque
CG_snapV
.
Lemma
CG_snap_type
st
l
Γ
τ
:
...
...
@@ -309,7 +309,7 @@ Section CG_Stack.
by
iFrame
.
Qed
.
Global
Typeclasses
Opaque
CG_snap
.
Typeclasses
Opaque
CG_snap
.
Global
Opaque
CG_snap
.
(* Coarse-grained iter *)
...
...
@@ -345,7 +345,7 @@ Section CG_Stack.
Lemma
CG_iter_of_val
f
:
of_val
(
CG_iterV
f
)
=
CG_iter
f
.
Proof
.
trivial
.
Qed
.
Global
Typeclasses
Opaque
CG_iterV
.
Typeclasses
Opaque
CG_iterV
.
Global
Opaque
CG_iterV
.
Lemma
CG_iter_subst
(
f
:
expr
)
g
:
(
CG_iter
f
).[
g
]
=
CG_iter
f
.[
g
].
...
...
@@ -386,7 +386,7 @@ Section CG_Stack.
iMod
(
do_step_pure
with
"[$Hj]"
)
as
"Hj"
;
eauto
.
Qed
.
Global
Typeclasses
Opaque
CG_iter
.
Typeclasses
Opaque
CG_iter
.
Global
Opaque
CG_iter
.
Lemma
CG_snap_iter_type
st
l
Γ
τ
:
...
...
@@ -420,7 +420,7 @@ Section CG_Stack.
Qed
.
Global
Typeclasses
Opaque
CG_snap_iter
.
Typeclasses
Opaque
CG_snap_iter
.
Global
Opaque
CG_snap_iter
.
Lemma
CG_stack_body_subst
(
st
l
:
expr
)
f
:
...
...
theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
View file @
636f6fb3
...
...
@@ -132,7 +132,7 @@ Section FG_stack.
Lemma
FG_push_of_val
st
:
of_val
(
FG_pushV
st
)
=
FG_push
st
.
Proof
.
trivial
.
Qed
.
Global
Typeclasses
Opaque
FG_pushV
.
Typeclasses
Opaque
FG_pushV
.
Global
Opaque
FG_pushV
.
Lemma
FG_push_type
st
Γ
τ
:
...
...
@@ -154,7 +154,7 @@ Section FG_stack.
Hint
Rewrite
FG_push_subst
:
autosubst
.
Global
Typeclasses
Opaque
FG_push
.
Typeclasses
Opaque
FG_push
.
Global
Opaque
FG_push
.
(* Fine-grained push *)
...
...
@@ -188,7 +188,7 @@ Section FG_stack.
Lemma
FG_pop_of_val
st
:
of_val
(
FG_popV
st
)
=
FG_pop
st
.
Proof
.
trivial
.
Qed
.
Global
Typeclasses
Opaque
FG_popV
.
Typeclasses
Opaque
FG_popV
.
Global
Opaque
FG_popV
.
Lemma
FG_pop_type
st
Γ
τ
:
...
...
@@ -220,7 +220,7 @@ Section FG_stack.
Hint
Rewrite
FG_pop_subst
:
autosubst
.
Global
Typeclasses
Opaque
FG_pop
.
Typeclasses
Opaque
FG_pop
.
Global
Opaque
FG_pop
.
(* Fine-grained iter *)
...
...
@@ -264,7 +264,7 @@ Section FG_stack.
Hint
Rewrite
FG_iter_subst
:
autosubst
.
Global
Typeclasses
Opaque
FG_iter
.
Typeclasses
Opaque
FG_iter
.
Global
Opaque
FG_iter
.
Lemma
FG_read_iter_type
st
Γ
τ
:
...
...
@@ -283,7 +283,7 @@ Section FG_stack.
Hint
Rewrite
FG_read_iter_subst
:
autosubst
.
Global
Typeclasses
Opaque
FG_read_iter
.
Typeclasses
Opaque
FG_read_iter
.
Global
Opaque
FG_read_iter
.
Lemma
FG_stack_body_type
st
Γ
τ
:
...
...
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