minor fixes

logsem · Jun 11, 2024 · 39c6ddf · 39c6ddf
1 parent 9f26c26
commit 39c6ddf
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git 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
@@ -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.