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
RefinedC
Commits
5b820b16
Commit
5b820b16
authored
Mar 09, 2021
by
Rodolphe Lepigre
Browse files
Rename [heap.v] into [ghost_state.v].
parent
53c8f253
Pipeline
#43131
passed with stage
in 16 minutes and 24 seconds
Changes
3
Pipelines
1
Hide whitespace changes
Inline
Side-by-side
theories/lang/
heap
.v
→
theories/lang/
ghost_state
.v
View file @
5b820b16
File moved
theories/lang/lifting.v
View file @
5b820b16
From
iris
.
proofmode
Require
Import
tactics
.
From
iris
.
program_logic
Require
Export
weakestpre
.
From
iris
.
program_logic
Require
Import
ectx_lifting
.
From
refinedc
.
lang
Require
Export
lang
heap
notation
.
From
refinedc
.
lang
Require
Export
lang
ghost_state
notation
.
From
refinedc
.
lang
Require
Import
tactics
.
Set
Default
Proof
Using
"Type"
.
Import
uPred
.
...
...
theories/typing/adequacy.v
View file @
5b820b16
...
...
@@ -2,7 +2,7 @@ From iris.program_logic Require Export adequacy weakestpre.
From
iris
.
algebra
Require
Import
csum
excl
auth
cmra_big_op
gmap
.
From
refinedc
.
typing
Require
Export
type
.
From
refinedc
.
typing
Require
Import
programs
function
bytes
globals
int
fixpoint
.
From
refinedc
.
lang
Require
Import
heap
.
From
refinedc
.
lang
Require
Import
ghost_state
.
From
iris
.
program_logic
Require
Export
language
.
Set
Default
Proof
Using
"Type"
.
...
...
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