X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskProof.v;h=e0cef35fab5fce577407222f7ffc677c6e08632c;hp=2afb2de11dd5eb4a5386cfa26c72405ab2a87ea6;hb=a0f1135d1a315b7bd876bb42cf80fc03645f4dae;hpb=7b2698b0dfe1d271a68a0efe2bf0d129b5f1f93e

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