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
Actris
Commits
528c3ed5
Commit
528c3ed5
authored
Jun 11, 2019
by
Jonas Kastberg Hinrichsen
Browse files
Refactoring: Renamed stype->proto files
parent
31346e33
Changes
9
Hide whitespace changes
Inline
Side-by-side
_CoqProject
View file @
528c3ed5
...
...
@@ -6,9 +6,9 @@ theories/proto/list.v
theories/proto/channel.v
theories/proto/involutive.v
theories/proto/side.v
theories/proto/
stype
_def.v
theories/proto/
stype
.v
theories/proto/
stype
_enc.v
theories/proto/
proto
_def.v
theories/proto/
proto_specs
.v
theories/proto/
proto
_enc.v
theories/proto/branching.v
theories/examples/examples.v
theories/examples/proofs.v
...
...
theories/examples/examples.v
View file @
528c3ed5
...
...
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
proto
Require
Import
stype
.
From
osiris
.
proto
Require
Import
proto_specs
.
Section
Examples
.
Context
`
{!
heapG
Σ
}
(
N
:
namespace
).
...
...
theories/examples/list_sort.v
View file @
528c3ed5
...
...
@@ -4,8 +4,8 @@ Require Import Omega.
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
osiris
.
proto
Require
Import
list
channel
stype_enc
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
proto
Require
Import
list
channel
proto_enc
.
Section
ListSortExample
.
Context
`
{!
heapG
Σ
}
`
{
logrelG
val
Σ
}
(
N
:
namespace
).
...
...
theories/examples/proofs.v
View file @
528c3ed5
...
...
@@ -2,7 +2,7 @@ From iris.proofmode Require Import tactics.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
proto
Require
Import
stype
.
From
osiris
.
proto
Require
Import
proto_specs
.
From
osiris
.
examples
Require
Import
examples
.
Section
ExampleProofs
.
...
...
theories/examples/proofs_enc.v
View file @
528c3ed5
...
...
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
algebra
Require
Import
list
auth
excl
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
proto
Require
Import
stype
_enc
.
From
osiris
.
proto
Require
Import
proto
_enc
.
From
osiris
.
examples
Require
Import
examples
.
Section
ExampleProofsEnc
.
...
...
theories/proto/branching.v
View file @
528c3ed5
...
...
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
algebra
Require
Import
list
auth
excl
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
proto
Require
Export
stype
_enc
.
From
osiris
.
proto
Require
Export
proto
_enc
.
Section
DualBranch
.
Context
`
{
PROP
:
bi
}.
...
...
theories/proto/
stype
_def.v
→
theories/proto/
proto
_def.v
View file @
528c3ed5
File moved
theories/proto/
stype
_enc.v
→
theories/proto/
proto
_enc.v
View file @
528c3ed5
...
...
@@ -3,7 +3,7 @@ From iris.program_logic Require Export weakestpre.
From
iris
.
heap_lang
Require
Import
proofmode
notation
.
From
iris
.
algebra
Require
Import
list
auth
excl
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
proto
Require
Export
encodable
stype
.
From
osiris
.
proto
Require
Export
encodable
proto_specs
.
Section
DualStypeEnc
.
Context
`
{
EncDec
V
}
`
{
PROP
:
bi
}
.
...
...
theories/proto/
stype
.v
→
theories/proto/
proto_specs
.v
View file @
528c3ed5
...
...
@@ -6,7 +6,7 @@ From iris.heap_lang.lib Require Import spin_lock.
From
iris
.
algebra
Require
Import
list
auth
excl
.
From
iris
.
base_logic
Require
Import
invariants
.
From
osiris
.
base_logic
Require
Import
auth_excl
.
From
osiris
.
proto
Require
Export
stype
_def
.
From
osiris
.
proto
Require
Export
proto
_def
.
From
osiris
.
proto
Require
Export
channel
.
Class
logrelG
A
Σ
:
=
{
...
...
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