summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--transp-inf110-02-typage.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/transp-inf110-02-typage.tex b/transp-inf110-02-typage.tex
index 4add232..188b7eb 100644
--- a/transp-inf110-02-typage.tex
+++ b/transp-inf110-02-typage.tex
@@ -3174,8 +3174,8 @@ $\inferrule*{
\inferrule*{
\inferrule*{ }{x_2:A_2\vdash x_2:A_2}
\\
-\inferrule*{ }{\_:C \vdash \_ [] : C}
-}{x_2:A_2;\_:A_2\to B \vdash \_ [x_2] : A_2\to B}
+\inferrule*{ }{\_:B \vdash \_ [] : B}
+}{x_2:A_2;\_:A_2\to B \vdash \_ [x_2] : B}
}{x_1:A_1, x_2:A_2;\_:C \vdash \_ [x_1; x_2] : B}
}{y:C, x_1:A_1, x_2:A_2\vdash y [x_1; x_2] : B}$
}