Commit 2afabce4 authored by Amin Timany's avatar Amin Timany

Remove the now unused Vlists

parent 5f2649fb
......@@ -2,7 +2,6 @@ Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
Require Import F_mu.lang F_mu.typing F_mu.rules F_mu.logrel.
Require Import prelude.Vlist.
Import uPred.
Section typed_interp.
......
......@@ -6,7 +6,6 @@ From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Require Import prelude.Vlist.
Import uPred.
Section typed_interp.
......
-Q . ""
prelude/base.v
prelude/Vlist.v
stlc/lang.v
stlc/typing.v
stlc/rules.v
......@@ -15,4 +14,4 @@ F_mu_ref/lang.v
F_mu_ref/typing.v
F_mu_ref/rules.v
F_mu_ref/logrel.v
F_mu_ref/fundamental.v
F_mu_ref/fundamental.v
\ No newline at end of file
This diff is collapsed.
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