X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrong.v;h=66295115a5f85d522b439fb613ac28380cbaa058;hp=874b368d80faac736c1e8146062a65beb852df4a;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=6282ce834832ba35e81d8019cae1ca38d187d07e

diff --git a/src/HaskStrong.v b/src/HaskStrong.v
index 874b368..6629511 100644
--- a/src/HaskStrong.v
+++ b/src/HaskStrong.v
@@ -47,8 +47,8 @@ Section HaskStrong.
   | ETyApp : ∀ Γ Δ κ σ τ ξ l,                    Expr Γ Δ ξ (HaskTAll κ σ) l                   -> Expr Γ Δ ξ (substT σ τ) l
   | ECoLam : forall Γ Δ κ σ (σ₁ σ₂:HaskType Γ κ) ξ l, Expr Γ (σ₁∼∼∼σ₂::Δ) ξ σ l    -> Expr Γ Δ ξ (σ₁∼∼σ₂    ⇒ σ) l
   | ECoApp : forall Γ Δ κ (σ₁ σ₂:HaskType Γ κ) (γ:HaskCoercion Γ Δ (σ₁∼∼∼σ₂)) σ ξ l, Expr Γ Δ ξ (σ₁ ∼∼ σ₂ ⇒ σ) l  -> Expr Γ Δ ξ σ l
-  | ETyLam : ∀ Γ Δ ξ κ σ l,
-    Expr (κ::Γ) (weakCE Δ) (weakLT○ξ) (HaskTApp (weakF σ) (FreshHaskTyVar _)) (weakL l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
+  | ETyLam : ∀ Γ Δ ξ κ σ l n,
+    Expr (list_ins n κ Γ) (weakCE_ Δ) (weakLT_○ξ) (HaskTApp (weakF_ σ) (FreshHaskTyVar_ _)) (weakL_ l)-> Expr Γ Δ ξ (HaskTAll κ σ) l
   | ECase    : forall Γ Δ ξ l tc tbranches atypes,
                Expr Γ Δ ξ (caseType tc atypes) l ->
                Tree ??{ sac : _
@@ -90,7 +90,7 @@ Section HaskStrong.
     | ETyApp  Γ Δ κ σ τ ξ l       e => "("+++exprToString e+++")@("+++toString τ+++")"
     | ECoApp Γ Δ κ σ₁ σ₂ γ σ ξ l e  => "("+++exprToString e+++")~(co)"
     | ECast Γ Δ ξ t1 t2 γ l e       => "cast ("+++exprToString e+++"):t2"
-    | ETyLam _ _ _ k _ _ e          => "\@_ ->"+++ exprToString e
+    | ETyLam _ _ _ k _ _ _ e        => "\@_ ->"+++ exprToString e
     | ECoLam Γ Δ κ σ σ₁ σ₂ ξ l e    => "\~_ ->"+++ exprToString e
     | ECase Γ Δ ξ l tc branches atypes escrut alts => "case " +++ exprToString escrut +++ " of FIXME"
     | ELetRec _ _ _ _ _ vars vu elrb e => "letrec FIXME in " +++ exprToString e