X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FHaskStrongToProof.v;h=e93ddd9978478a03d5ad2a8cc58420d6ed2f06c1;hp=8ae0d0920b8ca99e6f9c301bdb5075667dc2759a;hb=489b12c6c491b96c37839610d33fbdf666ee527f;hpb=6282ce834832ba35e81d8019cae1ca38d187d07e

diff --git a/src/HaskStrongToProof.v b/src/HaskStrongToProof.v
index 8ae0d09..e93ddd9 100644
--- a/src/HaskStrongToProof.v
+++ b/src/HaskStrongToProof.v
@@ -520,7 +520,7 @@ Fixpoint expr2antecedent {Γ'}{Δ'}{ξ'}{τ'}{l'}(exp:Expr Γ' Δ' ξ' τ' l') :
   | EBrak    Γ Δ ξ ec t lev e                     => expr2antecedent e
   | ECast    Γ Δ ξ γ t1 t2 lev      e             => expr2antecedent e
   | ENote    Γ Δ ξ t l n e                        => expr2antecedent e
-  | ETyLam   Γ Δ ξ κ σ l e                        => expr2antecedent e
+  | ETyLam   Γ Δ ξ κ σ l n e                      => expr2antecedent e
   | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => expr2antecedent e
   | ECoApp   Γ Δ κ γ σ₁ σ₂ σ ξ l      e           => expr2antecedent e
   | ETyApp   Γ Δ κ σ τ ξ  l    e                  => expr2antecedent e
@@ -1117,7 +1117,7 @@ Definition expr2proof  :
     | EBrak    Γ Δ ξ ec t lev e                     => let case_EBrak   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECast    Γ Δ ξ γ t1 t2 lev      e             => let case_ECast   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ENote    Γ Δ ξ t _ n e                        => let case_ENote   := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
-    | ETyLam   Γ Δ ξ κ σ l e                        => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
+    | ETyLam   Γ Δ ξ κ σ l n e                      => let case_ETyLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECoLam   Γ Δ κ σ σ₁ σ₂ ξ l             e      => let case_ECoLam  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ECoApp   Γ Δ κ σ₁ σ₂ σ γ ξ l      e           => let case_ECoApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)
     | ETyApp   Γ Δ κ σ τ ξ  l    e                  => let case_ETyApp  := tt in (fun e' => _) (expr2proof _ _ _ _ _ e)