Commit 667b497e authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Rename files.

parent 7c00a718
......@@ -10,10 +10,10 @@
theories/base.v
theories/types.v
theories/typing.v
theories/typed.v
theories/sem_types.v
theories/sem_type_formers.v
theories/sem_typing.v
theories/sem_typed.v
theories/compatibility.v
theories/fundamental.v
theories/safety.v
......
From tutorial_popl20 Require Export sem_typing.
From tutorial_popl20 Require Export sem_typed.
Section compatibility.
Context `{heapG Σ}.
......
From tutorial_popl20 Require Export typing compatibility interp.
From tutorial_popl20 Require Export typed compatibility interp.
Definition interp_env `{heapG Σ} (Γ : gmap string ty)
(ρ : list (sem_ty Σ)) : gmap string (sem_ty Σ) := flip interp ρ <$> Γ.
......
From tutorial_popl20 Require Export sem_typing.
From tutorial_popl20 Require Export sem_typed.
From tutorial_popl20 Require Import symbol_ghost two_state_ghost.
Section unsafe.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment