summaryrefslogtreecommitdiffstats
path: root/transp-inf110-03-quantif.tex
diff options
context:
space:
mode:
Diffstat (limited to 'transp-inf110-03-quantif.tex')
-rw-r--r--transp-inf110-03-quantif.tex4
1 files changed, 2 insertions, 2 deletions
diff --git a/transp-inf110-03-quantif.tex b/transp-inf110-03-quantif.tex
index 02917f0..770627e 100644
--- a/transp-inf110-03-quantif.tex
+++ b/transp-inf110-03-quantif.tex
@@ -445,7 +445,7 @@ donc), on notera $(\texttt{match~}z\texttt{~with~}\langle v,h\rangle
{\footnotesize (\textbf{N.B.} $v$ peut apparaître dans $s$ mais pas
dans $\Gamma$ ni $Q$.)}
\[
-\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}
+\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash s \;:\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}
\]
\medskip
@@ -494,7 +494,7 @@ $\forall$
\\\hline
$\exists$
&\scalebox{0.80}{$\inferrule{{\color{gray}\Gamma\vdash t:I}\\\Gamma\vdash z \;:\; Q[v\backslash t]}{\Gamma\vdash \langle t,z\rangle \;:\; \exists (v:I).\, Q}$}
-&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$}
+&\scalebox{0.80}{$\inferrule{\Gamma\vdash z \;:\; \exists (v:I).\, P\\\Gamma,\, v:I,\, h:P\vdash s \;:\; Q}{\Gamma\vdash (\texttt{match~}z\texttt{~with~}\langle v,h\rangle \mapsto s) \;:\; Q}$}
\\
\end{tabular}