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
Fengmin Zhu
Tutorial POPL20
Commits
1ba1810d
Commit
1ba1810d
authored
Jan 18, 2020
by
Robbert Krebbers
Browse files
Rename base into language.
parent
e15b0a11
Changes
4
Show whitespace changes
Inline
Side-by-side
_CoqProject
View file @
1ba1810d
...
...
@@ -8,7 +8,7 @@
# We have ambiguous paths and so far it is not even clear what they are (https://gitlab.mpi-sws.org/iris/iris/issues/240).
-arg -w -arg -ambiguous-paths
theories/
bas
e.v
theories/
languag
e.v
theories/types.v
theories/typed.v
theories/sem_types.v
...
...
theories/
bas
e.v
→
theories/
languag
e.v
View file @
1ba1810d
File moved
theories/sem_types.v
View file @
1ba1810d
From
tutorial_popl20
Require
Export
bas
e
.
From
tutorial_popl20
Require
Export
languag
e
.
From
iris
.
heap_lang
Require
Export
proofmode
.
From
iris
.
base_logic
.
lib
Require
Export
invariants
.
...
...
theories/types.v
View file @
1ba1810d
From
tutorial_popl20
Require
Export
bas
e
.
From
tutorial_popl20
Require
Export
languag
e
.
Inductive
ty
:
=
|
TVar
:
nat
→
ty
...
...
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