diff --git a/_CoqProject b/_CoqProject index f8241b5..0359382 100644 --- a/_CoqProject +++ b/_CoqProject @@ -24,7 +24,7 @@ theories/gitree/reify.v theories/gitree/greifiers.v theories/gitree/reductions.v theories/gitree/weakestpre.v -theories/gitree/hom.v +theories/hom.v theories/gitree.v theories/program_logic.v diff --git a/theories/examples/delim_lang/example.v b/theories/examples/delim_lang/example.v index 60d32fc..59f043d 100644 --- a/theories/examples/delim_lang/example.v +++ b/theories/examples/delim_lang/example.v @@ -1,4 +1,5 @@ From gitrees Require Import gitree lang_generic. +From gitrees.effects Require Import delim. From gitrees.examples.delim_lang Require Import lang interp. From iris.proofmode Require Import base classes tactics environments. From iris.base_logic Require Import algebra.