Commit 814354bc authored by Mickael Laurent's avatar Mickael Laurent
Browse files

some fixes

parent 78619fce
......@@ -133,7 +133,7 @@ The elements of $\Gamma\avdash\Gammap\ct e:t$ mean:
\qquad
\Infer[NoDef]
{ x\in\dom\Gammap\setminus\bv(e)\\
\Gamma\subst{x}{(\Gamma\land\Gammap)(x)} \avdash{\Gammap\setminus\{x\}}{\ct} e : S}
\Gamma\subst{x}{\Gamma(x)\land\Gammap(x)} \avdash{\Gammap\setminus\{x\}}{\ct} e : S}
{\Gamma \avdash\Gammap{\ct} e : S}
{ }
\\
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment