fix hom issues

theories/examples/delim_lang/hom.v

@@ -16,6 +16,11 @@ Section hom.
   Notation IT := (IT F R).
   Notation ITV := (ITV F R).
 
+  Program Definition 𝒫_HOM : HOM (A:=natO) := exist _ 𝒫 _.
+  Next Obligation.
+    apply _.
+  Qed.
+
   Program Definition AppContRSCtx_HOM {S : Set}
     (α : @interp_scope F R _ S -n> IT)
     (env : @interp_scope F R _ S)

theories/examples/delim_lang/logpred.v

@@ -213,11 +213,6 @@ Section logrel.
     iApply "H".
   Qed.
 
-  Program Definition 𝒫_HOM : @HOM sz CtxDep R _ rs := exist _ 𝒫 _.
-  Next Obligation.
-    apply _.
-  Qed.
-
   Lemma compat_shift {S : Set} (Γ : S -> ty) e σ α τ β :
     ⊢ valid (Γ ▹ (Tcont τ α)) e σ σ β -∗ valid Γ (interp_shift _ e) τ α β.
   Proof.

theories/examples/delim_lang/logrel.v

@@ -314,11 +314,6 @@ Section logrel.
     assumption.
   Qed.
 
-  Program Definition 𝒫_HOM : @HOM sz CtxDep R _ rs := exist _ 𝒫 _.
-  Next Obligation.
-    apply _.
-  Qed.
-
   Lemma compat_shift {S : Set} (Γ : S -> ty) e (e' : exprO (inc S)) σ α τ β :
     ⊢ valid (Γ ▹ (τ ⤑ α)) e e' σ σ β -∗ valid Γ (interp_shift _ e) (shift/cc e') τ α β.
   Proof.

theories/examples/input_lang_callcc/hom.v

@@ -1,5 +1,4 @@
-(** In this module, we package up IT homomorphism in a sigma type, and
-we will use it as a domain for logical relations on continuations *)
+(** Particular homomorphisms for the call/cc lang *)
 From gitrees Require Import gitree lang_generic.
 From gitrees Require Export hom.
 From gitrees.examples.input_lang_callcc Require Import lang interp.
@@ -74,8 +73,8 @@ Section hom.
   Qed.
 
   Program Definition OutputSCtx_HOM {S : Set}
-    (env : @interp_scope F A _ S)
-    : @HOM _ _ A _ _ := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
+    (env : @interp_scope F A _ S) : HOM (A:=natO)
+    := exist _ ((interp_outputk rs (λne env, idfun) env)) _.
   Next Obligation.
     intros; simpl.
     apply _.

theories/hom.v

@@ -1,3 +1,5 @@
+(** In this module, we package up IT homomorphism in a sigma type, and
+we will use it as a domain for logical relations on continuations *)
 From gitrees Require Import gitree lang_generic.
 Require Import Binding.Lib Binding.Set Binding.Env.