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
Joshua Yanovski
iris-coq
Commits
2769834f
Commit
2769834f
authored
Aug 10, 2016
by
Ralf Jung
Browse files
Merge branch 'typo' into 'master'
fix typo
@jung
good? See merge request
!2
parents
98e51974
f8e6e32e
Changes
1
Hide whitespace changes
Inline
Side-by-side
program_logic/model.v
View file @
2769834f
...
...
@@ -71,9 +71,9 @@ Notation "#[ Σ1 ; .. ; Σn ]" :=
(
**
*
Subfunctors
*
)
(
**
In
order
to
make
proofs
in
the
Iris
logic
modular
,
they
are
not
done
with
respect
to
some
concrete
list
of
functors
[
Σ
],
but
are
instead
parametrized
by
an
arbitrary
list
of
functors
[
Σ
]
that
contains
atleast
certain
functors
.
For
example
,
the
lock
library
is
parametrized
by
a
functor
[
Σ
]
that
should
have
:
the
functors
corresponding
to
:
the
heap
and
the
exclusive
monoid
to
manage
to
an
arbitrary
list
of
functors
[
Σ
]
that
contains
at
least
certain
functors
.
For
example
,
the
lock
library
is
paramet
e
rized
by
a
functor
[
Σ
]
that
should
have
the
functors
corresponding
to
the
heap
and
the
exclusive
monoid
to
manage
to
lock
invariant
.
The
contraints
to
can
be
expressed
using
the
type
class
[
subG
Σ
1
Σ
2
],
which
...
...
@@ -109,7 +109,7 @@ Qed.
(
**
*
Solution
of
the
recursive
domain
equation
*
)
(
**
We
first
declare
a
module
type
and
then
an
instance
of
it
so
as
to
seall
of
(
**
We
first
declare
a
module
type
and
then
an
instance
of
it
so
as
to
seal
al
l
of
the
construction
,
this
way
we
are
sure
we
do
not
use
any
properties
of
the
construction
,
and
also
avoid
Coq
from
blindly
unfolding
it
.
*
)
Module
Type
iProp_solution_sig
.
...
...
Write
Preview
Supports
Markdown
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