X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProofStratified.v;h=5c5f68a6ecd65998b05263c21d2a0ae4e7820d6b;hp=1f7d85dfb084313179b37cb92bf48ac55d4ee747;hb=77e8c70f4fd7a32db036fee5884a98208d450de2;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/HaskProofStratified.v b/src/HaskProofStratified.v
index 1f7d85d..5c5f68a 100644
--- a/src/HaskProofStratified.v
+++ b/src/HaskProofStratified.v
@@ -441,9 +441,9 @@ Section HaskProofStratified.
   Instance OrgPCF_ContextND_Relation Γ Δ lev : ContextND_Relation (PCF_sequent_join Γ Δ lev).
     admit.
     Defined.
-
+(*
   (* 5.1.3 *)
-  Instance PCF Γ Δ lev : @ProgrammingLanguage _ _ pcfjudg (PCFRule Γ Δ lev) :=
+  Instance PCF Γ Δ lev : @ProgrammingLanguage _ pcfjudg (PCFRule Γ Δ lev) :=
   { pl_eqv                := OrgPCF_ContextND_Relation Γ Δ lev
   ; pl_snd                := PCF_sequents Γ Δ lev
   }.
@@ -571,5 +571,5 @@ Section HaskProofStratified.
 *)
 admit.
     Defined.
-
+*)
 End HaskProofStratified.