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
Lennard Gäher
ReLoC
Commits
d829e1e2
Commit
d829e1e2
authored
Apr 08, 2019
by
Robbert Krebbers
Browse files
Bump Iris.
parent
f66e377a
Changes
2
Hide whitespace changes
Inline
Side-by-side
opam
View file @
d829e1e2
...
...
@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
depends: [
"coq-iris" { (= "dev.2019-0
3-26.0.0495f119
") | (= "dev") }
"coq-iris" { (= "dev.2019-0
4-07.4.4760ad33
") | (= "dev") }
"coq-autosubst" { = "dev.coq86" }
]
theories/typing/types.v
View file @
d829e1e2
...
...
@@ -68,7 +68,7 @@ Notation "∀: τ" :=
Notation
"∃: τ"
:
=
(
TExists
τ
%
ty
)
(
at
level
100
,
τ
at
level
200
)
:
FType_scope
.
Notation
"'ref' τ"
:
=
(
Tref
τ
%
ty
)
(
at
level
30
,
right
associativity
)
:
FType_scope
.
Notation
"'ref' τ"
:
=
(
Tref
τ
%
ty
)
(
at
level
10
)
:
FType_scope
.
(** * Typing judgements *)
Reserved
Notation
"Γ ⊢ₜ e : τ"
(
at
level
74
,
e
,
τ
at
next
level
).
...
...
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