X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=f98800db63e803f955082fe9bd24a30f6193c871;hp=5e6fac410aba92eea16973986094f6e6c6040a7f;hb=3282a2b78028238987a5a49e59d8e8d495aea0e1;hpb=d5f12624745edf327b49e515a1ebb5aeb265b70c

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 5e6fac4..f98800d 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -85,7 +85,7 @@ Inductive Rule : Tree ??Judg -> Tree ??Judg -> Type :=
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ ]@l]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ ]@l]
 
-| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > Σ₁,,(τ₂@@@lev) |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂ lev, Rule [Γ > Δ > (τ₂@@@lev),,Σ₁ |- (τ₂,,[τ₁]) @lev ] [Γ > Δ > Σ₁ |- [τ₁] @lev]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??{ sac : @StrongAltCon tc & @ProofCaseBranch tc Γ Δ lev tbranches avars sac }),
                    Rule