X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;fp=src%2FHaskProof.v;h=2b6aa3cb284378323bb827e7ee7bb6fa2a77f634;hp=a8b311e162ee7a12f127f05440d3d52fa492164f;hb=5deda3b8240059e9969a31706d89b8a3818b184c;hpb=a9a60dc234f76a4740b32c0f62aa0fe3a89fea83

diff --git a/src/HaskProof.v b/src/HaskProof.v
index a8b311e..2b6aa3c 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -36,7 +36,7 @@ Inductive Judg  :=
 (* information needed to define a case branch in a HaskProof *)
 Record ProofCaseBranch {tc:TyCon}{Γ}{Δ}{lev}{branchtype : HaskType Γ ★}{avars}{sac:@StrongAltCon tc} :=
 { pcb_freevars       :  Tree ??(LeveledHaskType Γ ★)
-; pcb_judg           := sac_Γ sac Γ > sac_Δ sac Γ avars (map weakCK' Δ)
+; pcb_judg           := sac_gamma sac Γ > sac_delta sac Γ avars (map weakCK' Δ)
                 > (mapOptionTree weakLT' pcb_freevars),,(unleaves (map (fun t => t@@weakL' lev)
                   (vec2list (sac_types sac Γ avars))))
                 |- [weakLT' (branchtype @@ lev)]