From: Adam Megacz <megacz@cs.berkeley.edu>
Date: Sat, 19 Mar 2011 21:15:17 +0000 (-0700)
Subject: change LetRec rule to allow only a single expression in the body
X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=commitdiff_plain;h=a0f1135d1a315b7bd876bb42cf80fc03645f4dae

change LetRec rule to allow only a single expression in the body
---

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 2afb2de..e0cef35 100644
--- a/src/HaskProof.v
+++ b/src/HaskProof.v
@@ -109,7 +109,7 @@ HaskCoercion Γ Δ (σ₁∼∼∼σ₂) ->
 | RAbsCo  : forall Γ Δ Σ κ (σ₁ σ₂:HaskType Γ κ) σ l,
    Rule [Γ > ((σ₁∼∼∼σ₂)::Δ)            > Σ |- [σ @@ l]]
         [Γ > Δ >                         Σ |- [σ₁∼∼σ₂⇒ σ @@l]]
-| RLetRec        : ∀ Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- τ₁,,τ₂ ] [Γ > Δ > Σ₁ |- τ₁ ]
+| RLetRec        : forall Γ Δ Σ₁ τ₁ τ₂, Rule [Γ > Δ > Σ₁,,τ₂ |- [τ₁],,τ₂ ] [Γ > Δ > Σ₁ |- [τ₁] ]
 | RCase          : forall Γ Δ lev tc Σ avars tbranches
   (alts:Tree ??(@ProofCaseBranch tc Γ Δ lev tbranches avars)),
                    Rule