Moved Vlist to prelude.

F_mu/fundamental.v

@@ -2,7 +2,7 @@ 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 Vlist.
+Require Import prelude.Vlist.
 Import uPred.
 
 Section typed_interp.

F_mu/logrel.v

@@ -2,7 +2,7 @@ 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.
-Require Import Vlist.
+Require Import prelude.Vlist.
 Import uPred.
 
 (** interp : is a unary logical relation. *)

F_mu_ref/fundamental.v

@@ -6,7 +6,7 @@ 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 Vlist.
+Require Import prelude.Vlist.
 Import uPred.
 
 Section typed_interp.

F_mu_ref/logrel.v

@@ -6,7 +6,7 @@ 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 Vlist.
+Require Import prelude.Vlist.
 Import uPred.
 
 (** interp : is a unary logical relation. *)

_CoqProject

 -Q . ""
 prelude/base.v
+prelude/Vlist.v
 stlc/lang.v
 stlc/typing.v
 stlc/rules.v
 stlc/logrel.v
 stlc/fundamental.v
-Vlist.v
 F_mu/lang.v
 F_mu/typing.v
 F_mu/rules.v