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

[coq-hetmet.git] / src / HaskProof.v

diff --git a/src/HaskProof.v b/src/HaskProof.v
index 2afb2de..e0cef35 100644 (file)
--- 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