Skip to content
GitLab
Projects
Groups
Snippets
Help
Loading...
Help
What's new
10
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in / Register
Toggle navigation
Open sidebar
FP
iris-atomic
Commits
db15fbd7
Commit
db15fbd7
authored
Feb 22, 2018
by
Jacques-Henri Jourdan
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Bump Iris, fix build.
parent
dda9060d
Pipeline
#9311
passed with stage
in 2 minutes and 52 seconds
Changes
2
Pipelines
103
Hide whitespace changes
Inline
Side-by-side
Showing
2 changed files
with
2 additions
and
2 deletions
+2
-2
opam
opam
+1
-1
theories/peritem.v
theories/peritem.v
+1
-1
No files found.
opam
View file @
db15fbd7
...
...
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_atomic"]
depends: [
"coq-iris" { (= "dev.201
7-12-18
.1") | (= "dev") }
"coq-iris" { (= "dev.201
8-02-21
.1") | (= "dev") }
]
theories/peritem.v
View file @
db15fbd7
...
...
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
From
iris
.
algebra
Require
Import
frac
auth
gmap
csum
.
From
iris
.
base_logic
Require
Import
big_op
.
From
iris_atomic
Require
Export
treiber
misc
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
namespaces
.
From
iris
.
base_logic
.
lib
Require
Import
invariants
.
Section
defs
.
Context
`
{
heapG
Σ
}
(
N
:
namespace
).
...
...
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