ebproof (20aug20)

git-svn-id: svn://tug.org/texlive/trunk@56139 c570f23f-e606-0410-a88d-b1316a301751

6 files changed, 1980 insertions, 1211 deletions

diff --git a/Master/texmf-dist/doc/latex/ebproof/README.md b/Master/texmf-dist/doc/latex/ebproof/README.md
index 0f8b35038cf..e794db1feed 100644
--- a/Master/texmf-dist/doc/latex/ebproof/README.md
+++ b/Master/texmf-dist/doc/latex/ebproof/README.md
@@ -14,9 +14,9 @@ styles of inference rules, placement of labels, etc.
 
 The distribution includes the following files:
 
-- `ebproof.sty` : the package
-- `ebproof.pdf` : the documentation
-- `ebproof.tex` : the LaTeX source for the documentation
+- `ebproof.dtx` : the doctrip source for the package and documentation
+- `ebproof.pdf` : the compiled documentation
+- `ebproof.sty` : the generated package
 
 The package requires `expl3` (the LaTeX3 programming environment) which
 provides many useful programming tools.
@@ -25,7 +25,7 @@ provides many useful programming tools.
 License
 -------
 
-Copyright 2015 Emmanuel Beffara <manu@beffara.org>
+Copyright 2015-2020 Emmanuel Beffara <manu@beffara.org>
 
 This work may be distributed and/or modified under the
 conditions of the LaTeX Project Public License, either version 1.3
@@ -39,4 +39,4 @@ This work has the LPPL maintenance status “maintained”.
 
 The Current Maintainer of this work is Emmanuel Beffara.
 
-This work consists of the files `ebproof.sty` and `ebproof.tex`.
+This work consists of the file `ebproof.dtx`.
diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
index e4c8d03b25e..60d433b9fd9 100644
--- a/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
+++ b/Master/texmf-dist/doc/latex/ebproof/ebproof.pdf
diff --git a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex b/Master/texmf-dist/doc/latex/ebproof/ebproof.tex
deleted file mode 100644
index eeb93e5cdff..00000000000
--- a/Master/texmf-dist/doc/latex/ebproof/ebproof.tex
+++ /dev/null
@@ -1,638 +0,0 @@
-%% ebproof.sty
-%% Copyright 2017 Emmanuel Beffara <manu@beffara.org>
-%
-% This work may be distributed and/or modified under the
-% conditions of the LaTeX Project Public License, either version 1.3
-% of this license or (at your option) any later version.
-% The latest version of this license is in
-%   http://www.latex-project.org/lppl.txt
-% and version 1.3 or later is part of all distributions of LaTeX
-% version 2005/12/01 or later.
-%
-% This work has the LPPL maintenance status `maintained'.
-%
-% The Current Maintainer of this work is Emmanuel Beffara.
-%
-% This work consists of the files ebproof.sty and ebproof.tex.
-
-\documentclass{article}
-
-\DeclareRobustCommand\package[1]{\texttt{#1}}
-
-\title{The \package{ebproof} package}
-\author{Emmanuel Beffara \\ \url{manu@beffara.org}}
-\date{Version 2.0 \\ March 17, 2017}
-
-\usepackage{amssymb}
-\usepackage{color}
-\usepackage{fancyvrb}
-\usepackage[a4paper]{geometry}
-\usepackage[colorlinks=true,urlcolor=blue]{hyperref}
-\usepackage{multicol}
-
-\usepackage{tikz}
-\usetikzlibrary{decorations.pathmorphing}
-
-\usepackage{ebproof}
-
-\newcommand\lit[1]{\texttt{#1}}
-\newcommand\cs[1]{\lit{\char`\\#1}}
-\newcommand\env[1]{\lit{#1}}
-\newcommand\opt[1]{\lit{#1}}
-\newcommand\meta[1]{$\langle$\textit{#1}$\rangle$}
-\newcommand\oarg[1]{\lit[\meta{#1}\lit]}
-\newcommand\marg[1]{\lit{\{}\meta{#1}\lit{\}}}
-
-\newenvironment{csdoc}[1]{%
-  \smallbreak\noindent{#1}%
-  \begin{list}{}{%
-    \topsep=1ex%
-  }%
-  \item
-}{%
-  \end{list}%
-}
-
-\newenvironment{example}[1]{%
-  \def\exampleoptions{#1}%
-  \VerbatimOut{example.tex}}{%
-  \endVerbatimOut
-  \begin{center}
-  \begin{minipage}{.4\textwidth}
-    \input{example.tex}
-  \end{minipage}%
-  \begin{minipage}{.6\textwidth}
-    \small
-    \expandafter\VerbatimInput\expandafter[\exampleoptions]{example.tex}
-  \end{minipage}%
-  \end{center}
-}
-
-\setcounter{tocdepth}{2}
-
-\begin{document}
-\maketitle
-
-\begin{multicols}{2}
-  \tableofcontents
-\end{multicols}
-
-\section{Introduction}
-
-The \env{ebproof} package provides commands to typeset proof trees, in the
-style of sequent calculus and related systems:
-
-\begin{example}{gobble=2}
-  \begin{prooftree}
-    \hypo{ \Gamma, A &\vdash B }
-    \infer1[abs]{ \Gamma &\vdash A\to B }
-    \hypo{ \Gamma \vdash A }
-    \infer2[app]{ \Gamma \vdash B }
-  \end{prooftree}
-\end{example}
-
-The structure is very much inspired by the
-\href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\package{bussproofs}}
-package, in particular for the postfix notation.
-I actually wrote \package{ebproof} because there were some limitations in
-\package{bussproofs} that I did not know how to lift, and also because I did
-not like some choices in that package (and also because it was fun to write).
-
-\section{Environments}
-
-The package provides the \env{prooftree} environment, in a standard and
-starred variants.
-
-\begin{csdoc}{
-    \cs{begin}\lit{\{prooftree\}}\oarg{options}
-      \meta{statements}
-    \cs{end}\lit{\{prooftree\}}}
-  Typeset the proof tree described by the \meta{statements}, as described in
-  section~\ref{sec:statements}.
-  The \meta{options} provide default formatting options for the proof tree.
-  This environment can be used either in math mode or in text mode.
-  It produces a proof tree at the current position in the text flow.
-\end{csdoc}
-
-\begin{csdoc}{
-    \cs{begin}\lit{\{prooftree*\}}\oarg{options}
-      \meta{statements}
-    \cs{end}\lit{\{prooftree*\}}}
-  Typeset the proof on a line of its own; it is essentially equivalent to
-  wrapping the \env{prooftree} environment inside a displayed math
-  environment.
-\end{csdoc}
-
-\noindent
-The starred version is used in situations when a single proof will be
-displayed.
-The non-starred version is useful in order to integrate the proof into some
-larger structure, like two parts of a formula:
-
-\begin{example}{gobble=2}
-  \[
-    \begin{prooftree}
-      \infer0{ \vdash A }
-      \hypo{ \vdash B } \infer1{ \vdash B, C }
-      \infer2{ \vdash A\wedge B, C }
-    \end{prooftree}
-    \quad \rightsquigarrow \quad
-    \begin{prooftree}
-      \infer0{ \vdash A } \hypo{ \vdash B }
-      \infer2{ \vdash A\wedge B }
-      \infer1{ \vdash A\wedge B, C }
-    \end{prooftree}
-  \]
-\end{example}
-
-\section{Statements}
-\label{sec:statements}
-
-Statements describe proofs in postfix notation: when typesetting a proof tree
-whose last rule has, say, two premisses, you will first write statements for
-the subtree of the first premiss, then statements for the subtree of the
-second premiss, then a statement like \cs{infer2}\{\meta{conclusion}\} to
-build an inference with these two subtrees as premisses and the given text as
-conclusion.
-
-Hence statements operate on a stack of proof trees.
-At the beginning of a \lit{prooftree} environment, the stack is empty.
-At the end, it must contain exactly one tree, which is the one that will be
-printed.
-
-Note that the commands defined in this section only exist right inside
-\env{prooftree} environments.
-If you have a macro with the same name as one of the statements, for instance
-\cs{hypo}, then this macro will keep its meaning outside \env{prooftree}
-environments as well as inside the arguments of a statement.
-If you really need to access the statements in another context, you can can
-always call them by prefixing their names with \lit{ebproof}, for instance as
-\cs{ebproofhypo}.
-
-\subsection{Basic statements}
-
-The basic statements for building proofs are the following, where
-\meta{options} stands for arbitrary options as described in
-section~\ref{sec:options}.
-\begin{csdoc}{\cs{hypo}\oarg{options}\marg{text}}
-  Push a new proof tree consisting only in one conclusion line, with no
-  premiss and no line above, in other words a tree with only a leaf
-  (\cs{hypo} stands for \emph{hypothesis}).
-\end{csdoc}
-\begin{csdoc}{\cs{infer}\oarg{options}\marg{arity}\oarg{label}\marg{text}}
-  Build an inference step by taking some proof trees from the top of the
-  stack, assembling them with a rule joining their conclusions and putting a
-  new conclusion below.
-  The \meta{arity} is the number of sub-proofs, it may be any number
-  including 0 (in this case there will be a line above the conclusion but no
-  sub-proof).
-  If \meta{label} is present, it is used as the label on the right of the
-  inference line; it is equivalent to using the \opt{right label} option.
-\end{csdoc}
-
-The \meta{text} in these statements is the contents of the conclusion at the
-root of the tree that the statements create.
-It is typeset in math mode by default but any kind of formatting can be used
-instead, using the \opt{template} option.
-The \meta{label} text is formatted in horizontal text mode by default.
-
-Each proof tree has a vertical axis, used for alignment of successive steps.
-The position of the axis is deduced from the text of the conclusion at the
-root of the tree: if \meta{text} contains the alignment character \verb|&|
-then the axis is set at that position, otherwise the axis is set at the center
-of the conclusion text.
-The \cs{infer} statement makes sure that the axis of the premiss is at the
-same position as the axis of the conclusion.
-If there are several premisses, it places the axis at the center between the
-left of the leftmost conclusion and the right of the rightmost conclusion:
-
-\begin{example}{gobble=2}
-  \begin{prooftree}
-    \hypo{ &\vdash A, B, C }
-    \infer1{ A &\vdash B, C }
-    \infer1{ A, B &\vdash C }
-    \hypo{ D &\vdash E }
-    \infer2{ A, B, D &\vdash C, E }
-    \infer1{ A, B &\vdash C, D, E }
-    \infer1{ A &\vdash B, C, D, E }
-  \end{prooftree}
-\end{example}
-
-\begin{csdoc}{\cs{ellipsis}\marg{label}\marg{text}}
-  Typeset vertical dots, with a label on the right, and a new conclusion.
-  No inference lines are inserted.
-  \begin{example}{gobble=4}
-    \begin{prooftree}
-      \hypo{ \Gamma &\vdash A }
-      \ellipsis{foo}{ \Gamma &\vdash A, B }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-
-\subsection{Modifying proof trees}
-
-The following additional statements may be used to affect the format of the
-last proof tree on the stack:
-
-\begin{csdoc}{\cs{rewrite}\marg{code}}
-  Rewrite the proof while preserving its size and alignment. The \meta{code}
-  is typeset in horizontal mode, with the following control sequences defined:
-  \begin{itemize}
-  \item \cs{treebox} is a box register that contains the original material,
-  \item \cs{treemark}\marg{name} expands as the position of a given mark with
-    respect to the left of the box.
-  \end{itemize}
-  A simple use of this statement is to change the color of a proof tree:
-  \begin{example}{gobble=4}
-    \begin{prooftree}
-      \hypo{ \Gamma, A &\vdash B }
-      \infer1[abs]{ \Gamma &\vdash A\to B }
-      \rewrite{\color{red}\box\treebox}
-      \hypo{ \Gamma \vdash A }
-      \infer2[app]{ \Gamma \vdash B }
-    \end{prooftree}
-  \end{example}
-  Note the absence of spaces inside the call to \cs{rewrite}, because spaces
-  would affect the position of the tree box.
-  Note also that explicit use of \cs{treebox} is required to actually draw the
-  subtree.
-  Not using it will effectively not render the subtree, while still reserving
-  its space in the enclosing tree:
-  \begin{example}{gobble=4}
-    \begin{prooftree}
-      \hypo{ \Gamma, A &\vdash B }
-      \infer1[abs]{ \Gamma &\vdash A\to B }
-      \rewrite{}
-      \hypo{ \Gamma \vdash A }
-      \infer2[app]{ \Gamma \vdash B }
-    \end{prooftree}
-  \end{example}
-  This kind of manipulation is useful for instance in conjunction with the
-  \package{beamer} package to allow revealing subtrees of a proof tree
-  progressively in successive slides of a given frame.
-\end{csdoc}
-
-\begin{csdoc}{\cs{delims}\marg{left}\marg{right}}
-  Put left and right delimiters around the whole sub-proof, without changing
-  the alignment (the spacing is affected by the delimiters, however).
-  The \meta{left} text must contain an opening occurrence of \cs{left} and the
-  \meta{right} text must contain a matching occurrence of \cs{right}.
-  For instance, \verb|\delims{\left(}{\right)}| will put the
-  sub-proof between parentheses.
-  \begin{example}{gobble=4}
-    \begin{prooftree}
-      \hypo{ A_1 \vee \cdots \vee A_n }
-      \hypo{ [A_i] }
-      \ellipsis{}{ B }
-      \delims{ \left( }{ \right)_{1\leq i\leq n} }
-      \infer2{ B }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-\section{Options}
-\label{sec:options}
-
-The formatting of trees, conclusion texts and inference rules is affected by
-options, specified using the \LaTeX3 key-value system.
-All options are in the \lit{ebproof} module in the key tree.
-They can be set locally for a proof tree or for a single statement using
-optional arguments in the associated commands.
-
-\begin{csdoc}{\cs{ebproofset}\marg{options}}
-  Set some options.
-  The options will apply in the current scope; using this in preamble will
-  effectively set options globally.
-  Specific options may also be specified for each proof tree and for each
-  statement in a proof tree, using optional arguments.
-\end{csdoc}
-
-\subsection{General shape}
-
-The options in this section only make sense at the global level and at the
-proof level.
-Changing the proof style inside a \lit{proof} environment has undefined
-behaviour.
-
-\begin{csdoc}{\opt{proof style=}\meta{name}}
-  Set the general shape for representing proofs.
-  The following styles are provided:
-  \begin{csdoc}{\lit{upwards}}
-    This is the default style.
-    Proof trees grow upwards, with conclusions below and premisses above.
-  \end{csdoc}
-  \begin{csdoc}{\lit{downwards}}
-    Proof trees grow downwards, with conclusions above and premisses below.
-    \begin{example}{gobble=4}
-      \begin{prooftree}[proof style=downwards]
-        \hypo{ \Gamma, A &\vdash B }
-        \infer1[abs]{ \Gamma &\vdash A\to B }
-        \hypo{ \Gamma \vdash A }
-        \infer2[app]{ \Gamma \vdash B }
-      \end{prooftree}
-    \end{example}
-  \end{csdoc}
-\end{csdoc}
-
-In the optional argument of \lit{prooftree} environments, proof styles can
-be specified directly, without prefixing the name by ``\lit{proof style=}''.
-For instance, the first line of the example above could be written
-\cs{begin}\lit{\{prooftree\}[downwards]} equivalently.
-
-\begin{csdoc}{\opt{center=}\meta{boolean}}
-  If set to \lit{true}, the tree produced by the \env{prooftree} environment
-  will be vertically centered around the text line.
-  If set to \lit{false}, the base line of the tree will be the base line of
-  the conclusion.
-  The default value is \lit{true}.
-  \begin{example}{gobble=4}
-    \begin{prooftree}[center=false]
-      \infer0{ A \vdash A }
-    \end{prooftree}
-    \qquad
-    \begin{prooftree}[center=false]
-      \hypo{ \Gamma, A \vdash B }
-      \infer1{ \Gamma \vdash A \to B }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-\subsection{Spacing}
-
-\begin{csdoc}{\opt{separation=}\meta{dimension}}
-  The horizontal separation between sub-proofs in an inference.
-  The default value is \lit{1.5em}.
-  \begin{example}{gobble=4}
-    \begin{prooftree}[separation=0.5em]
-      \hypo{ A } \hypo{ B } \infer2{ C }
-      \hypo{ D } \hypo{ E } \hypo{ F } \infer3{ G }
-      \hypo{ H } \infer[separation=3em]3{ K }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-\begin{csdoc}{\opt{rule margin=}\meta{dimension}}
-  The spacing above and below inference lines.
-  The default value is \lit{0.7ex}.
-  \begin{example}{gobble=4}
-    \begin{prooftree}[rule margin=2ex]
-      \hypo{ \Gamma, A &\vdash B }
-      \infer1[abs]{ \Gamma &\vdash A\to B }
-      \hypo{ \Gamma \vdash A }
-      \infer2[app]{ \Gamma \vdash B }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-\subsection{Shape of inference lines}
-
-\begin{csdoc}{\opt{rule style=}\meta{name}}
-  Set the shape of inference lines.
-  The following values are provided:
-  \begin{csdoc}{\opt{simple}}
-    A simple horizontal rule is drawn.
-    This is the default style.
-  \end{csdoc}
-  \begin{csdoc}{\opt{no rule}}
-    No inference line is drawn.
-    A single space of the length of \lit{rule margin} is inserted.
-  \end{csdoc}
-  \begin{csdoc}{\opt{double}}
-    A double line is drawn.
-  \end{csdoc}
-  \begin{csdoc}{\opt{dashed}}
-    A single dashed line is drawn.
-  \end{csdoc}
-  The precise rendering is influenced by parameters specified below.
-  Arbitrary new shapes can defined using the \lit{rule code} option described
-  below and the \cs{ebproofnewrulestyle} command described in
-  section~\ref{sec:styles}.
-\end{csdoc}
-
-In the optional argument of the \cs{infer} statement, rule styles can be
-specified directly, without prefixing the style name by ``\lit{rule style=}''.
-For instance, \cs{infer}\lit{[dashed]} is equivalent to
-\cs{infer}\lit{[rule style=dashed]}.
-
-\begin{example}{gobble=2}
-  \begin{prooftree}
-    \hypo{ \Gamma &\vdash A \to B }
-    \infer[no rule]1{ \Gamma &\vdash {!A} \multimap B }
-    \hypo{ \Delta &\vdash A }
-    \infer[rule thickness=2pt]1{ \Delta &\vdash {!A} }
-    \infer0{ B \vdash B }
-    \infer[dashed]2{ \Delta, {!A}\multimap B \vdash B }
-    \infer2{ \Gamma, \Delta &\vdash B }
-    \infer[double]1{ \Gamma \cup \Delta &\vdash B }
-  \end{prooftree}
-\end{example}
-
-\begin{csdoc}{\opt{rule thickness=}\meta{dimension}}
-  The thickness of inference lines.
-  It is \lit{0.4pt} by default.
-\end{csdoc}
-\begin{csdoc}{\opt{rule separation=}\meta{dimension}}
-  The distance between the two lines in the \lit{double} rule style.
-  It is \lit{2pt} by default.
-\end{csdoc}
-\begin{csdoc}{\opt{rule dash length=}\meta{dimension}}
-  The length of dashes in the \lit{dashed} rule style.
-  It is \lit{0.2em} by default.
-\end{csdoc}
-\begin{csdoc}{\opt{rule dash space=}\meta{dimension}}
-  The space between dashes in the \lit{dashed} rule style.
-  It is \lit{0.3em} by default.
-\end{csdoc}
-
-\begin{csdoc}{\opt{rule code=}\meta{code}}
-  This option is used to define an arbitrary shape for rules.
-  The \meta{code} is used to render the rule, it is executed in vertical mode
-  in a \cs{vbox} whose \cs{hsize} is set to the width of the rule.
-  Margins above and below are inserted automatically (they can be removed by
-  setting \lit{rule margin} to \lit{0pt}).
-
-  \begin{example}{gobble=4}
-    \begin{prooftree}[rule code={\hbox{\tikz
-        \draw[decorate,decoration={snake,amplitude=.3ex}]
-        (0,0) -- (\hsize,0);}}]
-      \hypo{ \Gamma &\vdash A }
-      \infer1{ \Gamma &\vdash A, \ldots, A }
-      \hypo{ \Delta, A, \ldots, A \vdash \Theta }
-      \infer2{ \Gamma, \Delta \vdash \Theta }
-    \end{prooftree}
-  \end{example}
-  Note that this example requires the \package{tikz} package, with the
-  \package{decorations.pathmorphing} library for the \lit{snake} decoration.
-\end{csdoc}
-
-\subsection{Format of conclusions}
-
-\begin{csdoc}{%
-    \opt{template=}\meta{code} \\
-    \opt{left template=}\meta{code} \\
-    \opt{right template=}\meta{code}}
-  Defines how conclusions are formatted.
-  The code is arbitrary \TeX\ code, composed in horizontal mode.
-  The macro \cs{inserttext} is used to insert the actual text passed to the
-  \cs{hypo} and \cs{infer} statements.
-  The \opt{template} value is used for conclusions with no alignment mark.
-  The \opt{left template} and \opt{right template} values are used on the left
-  and right side of the alignment mark when it is present.
-  The default value for \opt{template} is simply \verb|$\inserttext$|, so that
-  conclusions are set in math mode.
-  The default values for \opt{left template} and \opt{right template} are
-  similar, with spacing assuming that a relation symbol is put near the
-  alignment mark, so that \verb|\infer1{A &\vdash B}| is spaced correctly.
-
-  \begin{example}{gobble=4}
-    \begin{prooftree}[template=(\textbf\inserttext)]
-      \hypo{ foo }
-      \hypo{ bar }
-      \infer1{ baz }
-      \infer2{ quux }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-\subsection{Format of labels}
-
-\begin{csdoc}{%
-    \opt{left label=}\meta{text} \\
-    \opt{right label=}\meta{text}}
-  The text to use as the labels of the rules, on the left and on the right
-  of the inference line.
-  Using the second optional argument in \cs{infer} is equivalent to setting
-  the \env{right label} option with the value of that argument.
-
-  \begin{example}{gobble=4}
-    \begin{prooftree}
-      \hypo{ \Gamma, A &\vdash B }
-      \infer[left label=$\lambda$]1[abs]
-        { \Gamma &\vdash A\to B }
-      \hypo{ \Gamma \vdash A }
-      \infer[left label=@]2[app]{ \Gamma \vdash B }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-\begin{csdoc}{%
-    \opt{left label template=}\meta{code} \\
-    \opt{right label template=}\meta{code}}
-  Defines how rule labels are formatted.
-  The code is arbitrary \TeX\ code, composed in horizontal mode.
-  The macro \cs{inserttext} can be used to insert the actual label text, as
-  defined by the options above.
-  The default values are simply \cs{inserttext} so that labels are set in
-  plain text mode.
-\end{csdoc}
-
-\begin{csdoc}{\opt{label separation=}\meta{dimension}}
-  The spacing between an inference lines and its labels.
-  The default value is \lit{0.5em}.
-\end{csdoc}
-\begin{csdoc}{\opt{label axis=}\meta{dimension}}
-  The height of the horizontal axis used for aligning the labels with the
-  rules. The default value is \lit{0.5ex}.
-\end{csdoc}
-
-
-\subsection{Style macros}
-\label{sec:styles}
-
-The following commands allow for the definition of custom styles using the
-basic style options, in a way similar to PGF's ``styles'' and \LaTeX3's
-``meta-keys''.
-This allows setting a bunch of options with the same values in many proofs
-using a single definition.
-
-\begin{csdoc}{\cs{ebproofnewstyle}\marg{name}\marg{options}}
-  Define a new style option \meta{name} that sets the given \meta{options}.
-
-  For instance, the following code defines a new option \opt{small} that sets
-  various parameters so that proofs are rendered smaller.
-  \begin{example}{gobble=4}
-    \ebproofnewstyle{small}{
-      separation = 1em, rule margin = .5ex,
-      template = \footnotesize$\inserttext$ }
-    \begin{prooftree}[small]
-      \hypo{ \Gamma, A \vdash B }
-      \infer1{ \Gamma \vdash A\to B }
-      \hypo{ \Gamma \vdash A } \infer2{ \Gamma \vdash B }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-\begin{csdoc}{\cs{ebproofnewrulestyle}\marg{name}\marg{options}}
-  Define a new rule style.
-  The \meta{options} part includes options used to set how to draw rules in
-  the new style.
-
-  The option \opt{rule code} is useful in this command as it allows to
-  define arbitrary rule styles.
-  For instance, the squiggly rule example above could be turned into a new
-  rule style \lit{zigzag} with the following code:
-  \begin{example}{gobble=4}
-    \ebproofnewrulestyle{zigzag}{
-      rule code = {\hbox{\tikz
-        \draw[decorate,decoration={snake,amplitude=.3ex}]
-        (0,0) -- (\hsize,0);}}}
-    \begin{prooftree}
-      \hypo{ \Gamma &\vdash A }
-      \infer1{ \Gamma &\vdash A, \ldots, A }
-      \hypo{ \Delta, A, \ldots, A \vdash \Theta }
-      \infer[zigzag]2{ \Gamma, \Delta \vdash \Theta }
-    \end{prooftree}
-  \end{example}
-\end{csdoc}
-
-
-\section{License}
-
-This work may be distributed and/or modified under the
-conditions of the \LaTeX\ Project Public License, either version 1.3
-of this license or (at your option) any later version.
-The latest version of this license is in
-\begin{center}
-  \url{http://www.latex-project.org/lppl.txt}
-\end{center}
-and version 1.3 or later is part of all distributions of \LaTeX\
-version 2005/12/01 or later.
-
-This work has the LPPL maintenance status `maintained'.
-
-The Current Maintainer of this work is Emmanuel Beffara.
-
-This work consists of the files \texttt{ebproof.sty} and \texttt{ebproof.tex}.
-
-
-\section{History}
-
-This section lists the principal evolutions of the package, in reverse
-chronological order.
-\begin{description}
-\item[Version 2.0]
-  A complete rewrite of the code using the \LaTeX3 programming environment. 
-  The incompatible changes from the user's point of view are the following:
-  \begin{itemize}
-  \item Proof statements are now writtten in lowercase ({i.e.} \cs{Infer} is
-    now written \cs{infer} etc.) but the syntax is otherwise unchanged.
-    The old uppercase commands still work but produce a deprecation warning,
-    they will be removed in a future version.
-  \item New styles are now defined using \cs{ebproofnewstyle} and
-    \cs{ebproofnewrulestyle}. The previous method using PGF styles does not
-    work anymore (because PGF is not used anymore).
-  \end{itemize}
-  The new commands and options are the following:
-  \begin{itemize}
-  \item The statement \cs{rewrite} generalizes \cs{Alter},
-  \item The option \opt{label axis} controls vertical alignment of labels.
-  \end{itemize}
-\item[Version 1.1]
-  A bugfix release.
-  In \opt{template} options, one now uses \cs{inserttext} instead of \lit{\#1}
-  for the text arguments, which improves robustness.
-\item[Version 1.0]
-  The first public release.
-\end{description}
-
-\end{document}
diff --git a/Master/texmf-dist/source/latex/ebproof/ebproof.dtx b/Master/texmf-dist/source/latex/ebproof/ebproof.dtx
new file mode 100644
index 00000000000..71735ffc007
--- /dev/null
+++ b/Master/texmf-dist/source/latex/ebproof/ebproof.dtx
@@ -0,0 +1,1629 @@
+% \iffalse meta-comment
+%
+% Copyright (C) 2015-2020 by Emmanuel Beffara
+%
+% This file may be distributed and/or modified under the conditions of the
+% LaTeX Project Public License, either version 1.3 of this license or (at
+% your option) any later version. The latest version of this license is in:
+%
+%   http://www.latex-project.org/lppl.txt
+%
+% and version 1.3 or later is part of all distributions of LaTeX version
+% 2005/12/01 or later.
+%
+%<*driver>
+\documentclass[full]{l3doc}
+\usepackage{ebproof}
+\usepackage{multicol}
+\usepackage{tikz}
+\usetikzlibrary{decorations.pathmorphing}
+\EnableCrossrefs
+\newenvironment{example}{%
+  \VerbatimEnvironment
+  \begin{VerbatimOut}{example.tex}}{%
+  \end{VerbatimOut}
+  \begin{center}
+  \begin{minipage}{.4\textwidth}
+    \input{example.tex}
+  \end{minipage}%
+  \begin{minipage}{.6\textwidth}
+    \small\VerbatimInput[gobble=0]{example.tex}
+  \end{minipage}%
+  \end{center}
+}
+\begin{document}
+  \DocInput{\jobname.dtx}
+\end{document}
+%</driver>
+% \fi
+%
+% \title{^^A
+%   The \pkg{ebproof} package \\
+%   Formal proofs in the style of sequent calculus^^A
+% }
+%
+% \author{^^A
+%   Emmanuel Beffara\thanks
+%     {^^A
+%       E-mail:  \href{mailto:manu@beffara.org}{manu@beffara.org}^^A
+%     }^^A
+% }
+%
+% \date{Version 2.1 -- Released 2020-08-19}
+%
+% \maketitle
+%
+% \setcounter{tocdepth}{2}
+% \begin{multicols}{2}
+% \tableofcontents
+% \end{multicols}
+%
+% \begin{documentation}
+%
+% \section{Introduction}
+%
+% The \pkg{ebproof} package provides commands to typeset proof trees, in the
+% style of sequent calculus and related systems:
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ \Gamma, A &\vdash B }
+%     \infer1[abs]{ \Gamma &\vdash A\to B }
+%     \hypo{ \Gamma \vdash A }
+%     \infer2[app]{ \Gamma \vdash B }
+%   \end{prooftree}
+% \end{example}
+%
+% The structure is very much inspired by the
+% \href{http://math.ucsd.edu/~sbuss/ResearchWeb/bussproofs/}{\pkg{bussproofs}}
+% package, in particular for the postfix notation.
+% I actually wrote \pkg{ebproof} because there were some limitations in
+% \pkg{bussproofs} that I did not know how to lift, and also because I did
+% not like some choices in that package (and also because it was fun to write).
+%
+% Any feedback is welcome, in the form of bug reports, feature requests or
+% suggestions, through the web page of the project at \url{https://framagit.org/manu/ebproof}.
+%
+% \section{Environments}
+%
+% \begin{function}{prooftree,prooftree*}
+%   \begin{syntax}
+%     \verb|\begin{prooftree}|\oarg{options}
+%     ~ \meta{statements}
+%     \verb|\end{prooftree}|
+%   \end{syntax}
+%   The package provides the \env{prooftree} environment, in standard and
+%   starred variants.
+%   This typesets the proof tree described by the \meta{statements}, as
+%   described in section~\ref{sec:statements}.
+%   The \meta{options} provide default formatting options for the proof tree,
+%   available options are described in section~\ref{sec:options}.
+%
+%   Following the conventions of \pkg{amsmath} for alignment environments, the
+%   non-starred version produces a proof tree at the current position in the
+%   text flow (it can be used in math mode or text mode) while the starred
+%   version typesets the proof on a line of its own, like a displayed formula.
+% \end{function}
+%
+% \begin{example}
+%   \[
+%     \begin{prooftree}
+%       \infer0{ \vdash A }
+%       \hypo{ \vdash B } \infer1{ \vdash B, C }
+%       \infer2{ \vdash A\wedge B, C }
+%     \end{prooftree}
+%     \quad \rightsquigarrow \quad
+%     \begin{prooftree}
+%       \infer0{ \vdash A } \hypo{ \vdash B }
+%       \infer2{ \vdash A\wedge B }
+%       \infer1{ \vdash A\wedge B, C }
+%     \end{prooftree}
+%   \]
+% \end{example}
+%
+% \section{Statements}
+% \label{sec:statements}
+%
+% Statements describe proofs in postfix notation: when typesetting a proof tree
+% whose last rule has, say, two premisses, you will first write statements for
+% the subtree of the first premiss, then statements for the subtree of the
+% second premiss, then a statement like \cs{infer2}\{\meta{conclusion}\} to
+% build an inference with these two subtrees as premisses and the given text as
+% conclusion.
+%
+% Hence statements operate on a stack of proof trees.
+% At the beginning of a \env{prooftree} environment, the stack is empty.
+% At the end, it must contain exactly one tree, which is the one that will be
+% printed.
+%
+% Note that the commands defined in this section only exist right inside
+% \env{prooftree} environments.
+% If you have a macro with the same name as one of the statements, for instance
+% \cs{hypo}, then this macro will keep its meaning outside \env{prooftree}
+% environments as well as inside the arguments of a statement.
+% If you really need to access the statements in another context, you can can
+% always call them by prefixing their names with \texttt{ebproof}, for instance as
+% \cs{ebproofhypo}.
+%
+% \subsection{Basic statements}
+%
+% The basic statements for building proofs are the following, where
+% \meta{options} stands for arbitrary options as described in
+% section~\ref{sec:options}.
+%
+% \begin{function}{\hypo}
+%   \begin{syntax}
+%     \cs{hypo}\oarg{options}\marg{text}
+%   \end{syntax}
+%   The statement \cs{hypo} pushes a new proof tree consisting only in one
+%   conclusion line, with no premiss and no line above, in other words a tree
+%   with only a leaf (\cs{hypo} stands for \emph{hypothesis}).
+% \end{function}
+%
+% \begin{function}{\infer}
+%   \begin{syntax}
+%     \cs{infer}\oarg{options}\meta{arity}\oarg{label}\marg{text}
+%   \end{syntax}
+%   The statement \cs{infer} builds an inference step by taking some proof
+%   trees from the top of the stack, assembling them with a rule joining their
+%   conclusions and putting a new conclusion below.
+%   The \meta{arity} is the number of sub-proofs, it may be any number
+%   including 0 (in this case there will be a line above the conclusion but no
+%   sub-proof).
+%   If \meta{label} is present, it is used as the label on the right of the
+%   inference line; it is equivalent to using the \cmd{right label} option.
+% \end{function}
+%
+% \medskip
+%
+% The \meta{text} in these statements is the contents of the conclusion at the
+% root of the tree that the statements create.
+% It is typeset in math mode by default but any kind of formatting can be used
+% instead, using the \cmd{template} option.
+% The \meta{label} text is formatted in horizontal text mode by default.
+%
+% Each proof tree has a vertical axis, used for alignment of successive steps.
+% The position of the axis is deduced from the text of the conclusion at the
+% root of the tree: if \meta{text} contains the alignment character \verb|&|
+% then the axis is set at that position, otherwise the axis is set at the center
+% of the conclusion text.
+% The \cs{infer} statement makes sure that the axis of the premiss is at the
+% same position as the axis of the conclusion.
+% If there are several premisses, it places the axis at the center between the
+% left of the leftmost conclusion and the right of the rightmost conclusion:
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ &\vdash A, B, C }
+%     \infer1{ A &\vdash B, C }
+%     \infer1{ A, B &\vdash C }
+%     \hypo{ D &\vdash E }
+%     \infer2{ A, B, D &\vdash C, E }
+%     \infer1{ A, B &\vdash C, D, E }
+%     \infer1{ A &\vdash B, C, D, E }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{function}{\ellipsis}
+%   \begin{syntax}
+%     \cs{ellipsis}\marg{label}\marg{text}
+%   \end{syntax}
+%   The statement \cs{ellipsis} typesets vertical dots, with a label on the right,
+%   and a new conclusion. No inference lines are inserted.
+% \end{function}
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ \Gamma &\vdash A }
+%     \ellipsis{foo}{ \Gamma &\vdash A, B }
+%   \end{prooftree}
+% \end{example}
+%
+%
+% \subsection{Modifying proof trees}
+%
+% The following additional statements may be used to affect the format of the
+% last proof tree on the stack.
+%
+% \begin{function}{\rewrite}
+%   \begin{syntax}
+%     \cs{rewrite}\marg{code}
+%   \end{syntax}
+%   The statement \cs{rewrite} is used to modify the proof of the stack while
+%   preserving its size and alignment.
+%   The \meta{code} is typeset in horizontal mode, with the following control
+%   sequences defined:
+%   \begin{itemize}
+%   \item \cs{treebox} is a box register that contains the original material,
+%   \item \cs{treemark}\marg{name} expands as the position of a given mark with
+%     respect to the left of the box.
+%   \end{itemize}
+% \end{function}
+%
+% A simple use of this statement is to change the color of a proof tree:
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ \Gamma, A &\vdash B }
+%     \infer1[abs]{ \Gamma &\vdash A\to B }
+%     \rewrite{\color{red}\box\treebox}
+%     \hypo{ \Gamma \vdash A }
+%     \infer2[app]{ \Gamma \vdash B }
+%   \end{prooftree}
+% \end{example}
+% Note the absence of spaces inside the call to \cs{rewrite}, because spaces
+% would affect the position of the tree box.
+% Note also that explicit use of \cs{treebox} is required to actually draw the
+% subtree.
+% Not using it will effectively not render the subtree, while still reserving
+% its space in the enclosing tree:
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ \Gamma, A &\vdash B }
+%     \infer1[abs]{ \Gamma &\vdash A\to B }
+%     \rewrite{}
+%     \hypo{ \Gamma \vdash A }
+%     \infer2[app]{ \Gamma \vdash B }
+%   \end{prooftree}
+% \end{example}
+% This kind of manipulation is useful for instance in conjunction with the
+% \pkg{beamer} package to allow revealing subtrees of a proof tree
+% progressively in successive slides of a given frame.
+%
+% \begin{function}{\delims}
+%   \begin{syntax}
+%     \cs{delims}\marg{left}\marg{right}
+%   \end{syntax}
+%   The statement \cs{delims} puts left and right delimiters around the whole
+%   sub-proof, without changing the alignment (the spacing is affected by the
+%   delimiters, however).
+%   The \meta{left} text must contain an opening occurrence of \cs{left} and
+%   the \meta{right} text must contain a matching occurrence of \cs{right}.
+%   For instance, \verb|\delims{\left(}{\right)}| will put the sub-proof
+%   between parentheses.
+% \end{function}
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ A_1 \vee \cdots \vee A_n }
+%     \hypo{ [A_i] }
+%     \ellipsis{}{ B }
+%     \delims{ \left( }{ \right)_{1\leq i\leq n} }
+%     \infer2{ B }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{function}{\overlay}
+%   \begin{syntax}
+%     \cs{overlay}
+%   \end{syntax}
+%   The statement \cs{overlay} combines the last two proofs on the stack into
+%   a single one, so that their conclusions are placed at the same point.
+% \end{function}
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{Z}
+%     \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D}
+%       \rewrite{\color{blue}\box\treebox}
+%     \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I}
+%       \rewrite{\color{red}\box\treebox}
+%     \overlay \hypo{J} \infer3{K}
+%   \end{prooftree}
+% \end{example}
+%
+% The primary use of this feature is for building animated presentations where
+% a subtree in a proof has to be modified without affecting the general
+% alignment of the surrounding proof. For instance, the example above could be
+% used in Beamer to build successive slides in a given frame with two
+% different subtrees:
+%
+% \begin{verbatim}
+%   \begin{prooftree}
+%     \hypo{Z}
+%     \hypo{A} \hypo{B} \infer2{C} \hypo{D} \infer2{D}
+%       \only<2>{\rewrite{}} % erases this version on slide 2
+%     \hypo{E} \hypo{F} \hypo{G} \infer2{H} \infer2{I}
+%       \only<1>{\rewrite{}} % erases this version on slide 1
+%     \overlay \hypo{J} \infer3{K}
+%   \end{prooftree}
+% \end{verbatim}
+%
+% \section{Options}
+% \label{sec:options}
+%
+% The formatting of trees, conclusion texts and inference rules is affected by
+% options, specified using the \LaTeX3 key-value system.
+% All options are in the \texttt{ebproof} module in the key tree.
+% They can be set locally for a proof tree or for a single statement using
+% optional arguments in the associated commands.
+%
+% \begin{function}{\ebproofset,\set}
+%   \begin{syntax}
+%     \cs{ebproofset}\marg{options}
+%   \end{syntax}
+%   The statement \cs{ebproofset} is used to set some options. When used
+%   inside a \env{prooftree} environment, it can written \cs{set}.
+%   The options will apply in the current scope; using this in preamble will
+%   effectively set options globally.
+%   Specific options may also be specified for each proof tree and for each
+%   statement in a proof tree, using optional arguments.
+% \end{function}
+%
+% \subsection{General shape}
+%
+% The options in this section only make sense at the global level and at the
+% proof level.
+% Changing the proof style inside a \env{proof} environment has undefined
+% behaviour.
+%
+% \begin{variable}{proof style}
+%   The option \cmd{proof style} sets the general shape for representing proofs.
+%   The following styles are provided:
+%   \begin{description}
+%   \item[upwards] 
+%     This is the default style.
+%     Proof trees grow upwards, with conclusions below and premisses above.
+%   \item[downwards]
+%     Proof trees grow downwards, with conclusions above and premisses below.
+%     \fvset{gobble=6}
+%     \begin{example}
+%       \begin{prooftree}[proof style=downwards]
+%         \hypo{ \Gamma, A &\vdash B }
+%         \infer1[abs]{ \Gamma &\vdash A\to B }
+%         \hypo{ \Gamma \vdash A }
+%         \infer2[app]{ \Gamma \vdash B }
+%       \end{prooftree}
+%     \end{example}
+%   \end{description}
+% \end{variable}
+%
+% In the optional argument of \env{prooftree} environments, proof styles can
+% be specified directly, without prefixing the name by ``\texttt{proof style=}''.
+% For instance, the first line of the example above could be written
+% \verb|\begin{prooftree}| equivalently.
+%
+% \begin{variable}{center}
+%   The option \cmd{center} toggles vertical centering of typeset proofs.
+%   If set to \texttt{true}, the tree produced by the \env{prooftree}
+%   environment will be vertically centered around the text line.
+%   If set to \texttt{false}, the base line of the tree will be the base line
+%   of the conclusion.
+%   The default value is \texttt{true}.
+% \end{variable}
+%
+% \begin{example}
+%   \begin{prooftree}[center=false]
+%     \infer0{ A \vdash A }
+%   \end{prooftree}
+%   \qquad
+%   \begin{prooftree}[center=false]
+%     \hypo{ \Gamma, A \vdash B }
+%     \infer1{ \Gamma \vdash A \to B }
+%   \end{prooftree}
+% \end{example}
+%
+% \subsection{Spacing}
+%
+% \begin{variable}{separation}
+%   Horizontal separation between sub-proofs in an inference is defined by the
+%   option \cmd{separation}.
+%   The default value is \texttt{1.5em}.
+% \end{variable}
+%
+% \begin{example}
+%   \begin{prooftree}[separation=0.5em]
+%     \hypo{ A } \hypo{ B } \infer2{ C }
+%     \hypo{ D } \hypo{ E } \hypo{ F } \infer3{ G }
+%     \hypo{ H } \infer[separation=3em]3{ K }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{variable}{rule margin}
+%   The spacing above and below inference lines is defined by the option
+%   \cmd{rule margin}.
+%   The default value is \texttt{0.7ex}.
+% \end{variable}
+%
+% \begin{example}
+%   \begin{prooftree}[rule margin=2ex]
+%     \hypo{ \Gamma, A &\vdash B }
+%     \infer1[abs]{ \Gamma &\vdash A\to B }
+%     \hypo{ \Gamma \vdash A }
+%     \infer2[app]{ \Gamma \vdash B }
+%   \end{prooftree}
+% \end{example}
+%
+% \subsection{Shape of inference lines}
+%
+% \begin{variable}{rule style}
+%   The shape of inference lines is set by the option \cmd{rule style}.
+%   The following values are provided:
+%   \begin{center}
+%     \begin{tabular}{@{}l@{\qquad}l@{}}
+%       \toprule
+%       \cmd{simple}  & a simple line (this is the default style) \\
+%       \cmd{no rule} & no rule, only a single space of length \texttt{rule margin} \\
+%       \cmd{double}  & a double line \\
+%       \cmd{dashed}  & a single dashed line \\
+%       \bottomrule
+%     \end{tabular}
+%   \end{center}
+% \end{variable}
+%
+% The precise rendering is influenced by parameters specified below.
+% Arbitrary new shapes can defined using the \cs{ebproofnewrulestyle} command
+% described in section~\ref{sec:styles}, using \texttt{rule code} option
+% described below.
+%
+% In the optional argument of the \cs{infer} statement, rule styles can be
+% specified directly, without prefixing the style name by ``\texttt{rule style=}''.
+% For instance, \verb|\infer[dashed]| is equivalent to
+% \verb|\infer[rule style=dashed]|.
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ \Gamma &\vdash A \to B }
+%     \infer[no rule]1{ \Gamma &\vdash {!A} \multimap B }
+%     \hypo{ \Delta &\vdash A }
+%     \infer[rule thickness=2pt]1{ \Delta &\vdash {!A} }
+%     \infer0{ B \vdash B }
+%     \infer[dashed]2{ \Delta, {!A}\multimap B \vdash B }
+%     \infer2{ \Gamma, \Delta &\vdash B }
+%     \infer[double]1{ \Gamma \cup \Delta &\vdash B }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{variable}{rule thickness,rule separation}
+%   The thickness of inference lines is defined by option \cmd{rule
+%   thickness}, it is \texttt{0.4pt} by default.
+%   The distance between the two lines in the \texttt{double} rule style is
+%   defined by the \cmd{rule separation} option.
+%   It is \texttt{2pt} by default.
+% \end{variable}
+% \begin{variable}{rule dash length,rule dash space}
+%   For dashed rules, the length of dashes is defined by the option
+%   \cmd{rule dash length} and the space between dashes is defined by the
+%   option \cmd{rule dash space}.
+%   The default values are \texttt{0.2em} and \texttt{0.3em} respectively.
+% \end{variable}
+%
+% \begin{variable}{rule code}
+%   Arbitrary rule shapes can be optained using the \cmd{rule code} option.
+%   The argument is code is used to render the rule, it is executed in
+%   vertical mode in a \cs{vbox} whose \cs{hsize} is set to the width of the
+%   rule.
+%   Margins above and below are inserted automatically (they can be removed by
+%   setting \texttt{rule margin} to \texttt{0pt}).
+% \end{variable}
+%
+% \begin{example}
+%   \begin{prooftree}[rule code={\hbox{\tikz
+%       \draw[decorate,decoration={snake,amplitude=.3ex}]
+%       (0,0) -- (\hsize,0);}}]
+%     \hypo{ \Gamma &\vdash A }
+%     \infer1{ \Gamma &\vdash A, \ldots, A }
+%     \hypo{ \Delta, A, \ldots, A \vdash \Theta }
+%     \infer2{ \Gamma, \Delta \vdash \Theta }
+%   \end{prooftree}
+% \end{example}
+% Note that this example requires the \pkg{tikz} package, with the
+% \pkg{decorations.pathmorphing} library for the \texttt{snake} decoration.
+%
+% \subsection{Format of conclusions and labels}
+%
+% \begin{variable}{template,left template,right template}
+%   The format of text in inferences is defined by templates.
+%   The option \cmd{template} is used for text with no alignment mark, the
+%   options \cmd{left template} and \cmd{right template} are used for the left
+%   and right side of the alignment mark when it is present.
+%   The value of these options is arbitrary \TeX\ code, composed in horizontal mode.
+%   The macro \cs{inserttext} is used to insert the actual text passed to the
+%   \cs{hypo} and \cs{infer} statements.
+%   The default value for \cmd{template} is simply \verb|$\inserttext$|, so
+%   that conclusions are set in math mode.
+%   The default values for \cmd{left template} and \cmd{right template} are
+%   similar, with spacing assuming that a relation symbol is put near the
+%   alignment mark, so that \verb|\infer1{A &\vdash B}| is spaced correctly.
+% \end{variable}
+%
+% \begin{example}
+%   \begin{prooftree}[template=(\textbf\inserttext)]
+%     \hypo{ foo }
+%     \hypo{ bar }
+%     \infer1{ baz }
+%     \infer2{ quux }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{variable}{left label,right label}
+%   The text to use as the labels of the rules, on the left and on the right
+%   of the inference line, is defined by the options \cmd{left label} and
+%   \cmd{right label}.
+%   Using the second optional argument in \cs{infer} is equivalent to setting
+%   the \env{right label} option with the value of that argument.
+% \end{variable}
+%
+% \begin{example}
+%   \begin{prooftree}
+%     \hypo{ \Gamma, A &\vdash B }
+%     \infer[left label=$\lambda$]1[abs]
+%       { \Gamma &\vdash A\to B }
+%     \hypo{ \Gamma \vdash A }
+%     \infer[left label=@]2[app]{ \Gamma \vdash B }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{variable}{left label template,right label template}
+%   Similarly to conclusions, labels are formatted according to templates.
+%   The code is arbitrary \TeX\ code, composed in horizontal mode, where the
+%   macro \cs{inserttext} can be used to insert the actual label text.
+%   The default values are simply \cs{inserttext} so that labels are set in
+%   plain text mode.
+% \end{variable}
+% \begin{variable}{label separation}
+%   The spacing between an inference line and its labels is defined by the
+%   option \cmd{label separation}, the default value is \texttt{0.5em}.
+%   The height of the horizontal axis used for aligning the labels with the
+%   rules is defined by the option \cmd{label axis}, the default value is
+%   \texttt{0.5ex}.
+% \end{variable}
+%
+%
+% \subsection{Style macros}
+% \label{sec:styles}
+%
+% The following commands allow for the definition of custom styles using the
+% basic style options, in a way similar to PGF's ``styles'' and \LaTeX3's
+% ``meta-keys''.
+% This allows setting a bunch of options with the same values in many proofs
+% using a single definition.
+%
+% \begin{function}{\ebproofnewstyle}
+%   \begin{syntax}
+%     \cs{ebproofnewstyle}\marg{name}\marg{options}
+%   \end{syntax}
+%   The statement \cs{ebproofnewstyle} defines a new style option with some
+%   \meta{name} that sets a given set of \meta{options}.
+% \end{function}
+% For instance, the following code defines a new option \cmd{small} that sets
+% various parameters so that proofs are rendered smaller.
+% \begin{example}
+%   \ebproofnewstyle{small}{
+%     separation = 1em, rule margin = .5ex,
+%     template = \footnotesize$\inserttext$ }
+%   \begin{prooftree}[small]
+%     \hypo{ \Gamma, A \vdash B }
+%     \infer1{ \Gamma \vdash A\to B }
+%     \hypo{ \Gamma \vdash A } \infer2{ \Gamma \vdash B }
+%   \end{prooftree}
+% \end{example}
+%
+% \begin{function}{\ebproofnewrulestyle}
+%   \begin{syntax}
+%     \cs{ebproofnewrulestyle}\marg{name}\marg{options}
+%   \end{syntax}
+%   The statement \cs{ebproofnewrulestyle} does the same for rule styles.
+%   The \meta{options} part includes options used to set how to draw rules in
+%   the new style.
+% \end{function}
+%
+% The option \cmd{rule code} is useful in this command as it allows to
+% define arbitrary rule styles.
+% For instance, the squiggly rule example above could be turned into a new
+% rule style \texttt{zigzag} with the following code:
+% \begin{example}
+%   \ebproofnewrulestyle{zigzag}{
+%     rule code = {\hbox{\tikz
+%       \draw[decorate,decoration={snake,amplitude=.3ex}]
+%       (0,0) -- (\hsize,0);}}}
+%   \begin{prooftree}
+%     \hypo{ \Gamma &\vdash A }
+%     \infer1{ \Gamma &\vdash A, \ldots, A }
+%     \hypo{ \Delta, A, \ldots, A \vdash \Theta }
+%     \infer[zigzag]2{ \Gamma, \Delta \vdash \Theta }
+%   \end{prooftree}
+% \end{example}
+%
+%
+% \section{License}
+%
+% This work may be distributed and/or modified under the
+% conditions of the \LaTeX\ Project Public License, either version 1.3
+% of this license or (at your option) any later version.
+% The latest version of this license is in
+% \begin{center}
+%   \url{http://www.latex-project.org/lppl.txt}
+% \end{center}
+% and version 1.3 or later is part of all distributions of \LaTeX\
+% version 2005/12/01 or later.
+%
+% This work has the LPPL maintenance status `maintained'.
+%
+% The Current Maintainer of this work is Emmanuel Beffara.
+%
+% This work consists of the files \texttt{ebproof.sty} and \texttt{ebproof.tex}.
+%
+% \section{History}
+%
+% This section lists the principal evolutions of the package, in reverse
+% chronological order.
+% \begin{description}
+% \item[Version 2.1 (2020-08-19)]
+%   Mostly a bugfix release.
+%   \begin{itemize}
+%   \item Makes the \env{prooftree} environment robust to use in tabular
+%     contexts.
+%   \item Adds the \cs{overlay} statement.
+%   \item Fixes a compatibility issue with \LaTeX\ release 2020-10-01.
+%   \end{itemize}
+% \item[Version 2.0 (2017-05-17)]
+%   A complete rewrite of the code using the \LaTeX3 programming environment. 
+%   The incompatible changes from the user's point of view are the following:
+%   \begin{itemize}
+%   \item Proof statements are now writtten in lowercase ({i.e.} \cs{Infer} is
+%     now written \cs{infer} etc.) but the syntax is otherwise unchanged.
+%     The old uppercase commands still work but produce a deprecation warning,
+%     they will be removed in a future version.
+%   \item New styles are now defined using \cs{ebproofnewstyle} and
+%     \cs{ebproofnewrulestyle}. The previous method using PGF styles does not
+%     work anymore (because PGF is not used anymore).
+%   \end{itemize}
+%   The new commands and options are the following:
+%   \begin{itemize}
+%   \item The statement \cs{rewrite} generalizes \cs{Alter},
+%   \item The option \cmd{label axis} controls vertical alignment of labels.
+%   \end{itemize}
+% \item[Version 1.1 (2015-03-13)]
+%   A bugfix release.
+%   In \cmd{template} options, one now uses \cs{inserttext} instead of \verb|#1|
+%   for the text arguments, which improves robustness.
+% \item[Version 1.0 (2015-02-04)]
+%   The first public release.
+% \end{description}
+%
+% \end{documentation}
+%
+% \clearpage \appendix
+%
+% \begin{implementation}
+%
+% \section{Implementation}
+%
+%    \begin{macrocode}
+%<*package>
+\NeedsTeXFormat{LaTeX2e}
+\RequirePackage{expl3}
+\RequirePackage{xparse}
+\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees}
+%<@@=ebproof>
+%    \end{macrocode}
+%
+% \subsection{Parameters}
+%
+% We first declare all options. For the meaning of options, see
+% section~\ref{sec:options}.
+%
+%    \begin{macrocode}
+\keys_define:nn { ebproof } {
+center .bool_set:N = \l_@@_center_bool,
+proof~style .choice: ,
+proof~style / upwards .code:n = \bool_set_false:N \l_@@_updown_bool,
+proof~style / downwards .code:n = \bool_set_true:N \l_@@_updown_bool,
+separation .dim_set:N = \l_@@_separation_dim,
+rule~margin .dim_set:N = \l_@@_rule_margin_dim,
+rule~thickness .dim_set:N = \l_@@_rule_thickness_dim,
+rule~separation .dim_set:N = \l_@@_rule_separation_dim,
+rule~dash~length .dim_set:N = \l_@@_rule_dash_length_dim,
+rule~dash~space .dim_set:N = \l_@@_rule_dash_space_dim,
+rule~code .tl_set:N = \l_@@_rule_code_tl,
+rule~style .choice:,
+template .tl_set:N = \l_@@_template_tl,
+left~template .tl_set:N = \l_@@_left_template_tl,
+right~template .tl_set:N = \l_@@_right_template_tl,
+left~label .tl_set:N = \l_@@_left_label_tl,
+right~label .tl_set:N = \l_@@_right_label_tl,
+left~label~template .tl_set:N = \l_@@_left_label_template_tl,
+right~label~template .tl_set:N = \l_@@_right_label_template_tl,
+label~separation .dim_set:N = \l_@@_label_separation_dim,
+label~axis .dim_set:N = \l_@@_label_axis_dim,
+}
+%    \end{macrocode}
+%
+% \begin{macro}{\ebproofnewrulestyle}
+%   We then define the document-level macro \cs{ebproofnewrulestyle} and use
+%   it to define the default styles. This simply consists in defining a
+%   meta-key.
+%    \begin{macrocode}
+\NewDocumentCommand \ebproofnewrulestyle { mm } {
+  \keys_define:nn { ebproof } {
+    rule~style / #1 .meta:nn = { ebproof } { #2 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% The styles |simple|, |no rule| and |double| are defined in a straightforward
+% way.
+%
+%    \begin{macrocode}
+\ebproofnewrulestyle { simple } {
+  rule~code = { \tex_hrule:D height \l_@@_rule_thickness_dim }
+}
+\ebproofnewrulestyle { no~rule } {
+  rule~code =
+}
+\ebproofnewrulestyle { double } {
+  rule~code = {
+    \tex_hrule:D height \l_@@_rule_thickness_dim
+    \skip_vertical:N \l_@@_rule_separation_dim
+    \tex_hrule:D height \l_@@_rule_thickness_dim
+  }
+}
+%    \end{macrocode}
+%
+% The |dashed| style uses leaders and filling for repeating a single dash. We
+% use \TeX\ primitives that have no \LaTeX3 counterpart for this.
+%
+%    \begin{macrocode}
+\ebproofnewrulestyle { dashed } {
+  rule~code = {
+    \hbox_to_wd:nn { \tex_hsize:D } {
+      \dim_set:Nn \l_tmpa_dim { \l_@@_rule_dash_space_dim / 2 }
+      \skip_horizontal:n { -\l_tmpa_dim }
+      \tex_cleaders:D \hbox:n {
+        \skip_horizontal:N \l_tmpa_dim
+        \tex_vrule:D
+          height \l_@@_rule_thickness_dim
+          width \l_@@_rule_dash_length_dim
+        \skip_horizontal:N \l_tmpa_dim
+      } \tex_hfill:D
+      \skip_horizontal:n { -\l_tmpa_dim }
+    }
+  }
+}
+%    \end{macrocode}
+%
+% Now we can define the default values, including the default rule style.
+%
+%    \begin{macrocode}
+\keys_set:nn { ebproof } {
+  center = true,
+  proof~style = upwards,
+  separation = 1.5em,
+  rule~margin = .7ex,
+  rule~thickness = .4pt,
+  rule~separation = 2pt,
+  rule~dash~length = .2em,
+  rule~dash~space = .3em,
+  rule~style = simple,
+  template = $\inserttext$,
+  left~template = $\inserttext\mathrel{}$,
+  right~template = $\mathrel{}\inserttext$,
+  left~label = ,
+  right~label = ,
+  left~label~template = \inserttext,
+  right~label~template = \inserttext,
+  label~separation = 0.5em,
+  label~axis = 0.5ex
+}
+%    \end{macrocode}
+%
+% \begin{macro}{\ebproofnewstyle}
+%   Defining a style simply means defining a meta-key.
+%    \begin{macrocode}
+\NewDocumentCommand \ebproofnewstyle { mm } {
+  \keys_define:nn { ebproof } { #1 .meta:n = { #2 } }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+%
+% \subsection{Proof boxes}
+%
+% \TeX\ does not actually provide data structures, so we have to encode things.
+% We provide an allocator for ``registers'' holding boxes with attributes. Such
+% a register consists in a box register and a property list for marks, which
+% maps mark names to values as explicit dimensions with units.
+%
+% \begin{macro}{\@@_new:N}
+%   Using only public interfaces forces a convoluted approach to allocation:
+%   we use a global counter \cs{g_ebproof_register_int} to number registers,
+%   then each allocation creates registers named \cs{g_ebproof_K_N} where K is
+%   the kind of component (box or marks) and N is the identifier of the
+%   register. The proof box register itself only contains the identifier used
+%   for indirection.
+%    \begin{macrocode}
+\int_new:N \g_@@_register_int
+\cs_new:Nn \@@_box:N { g__ebproof_box_ \tl_use:N #1 }
+\cs_new:Nn \@@_marks:N { g__ebproof_marks_ \tl_use:N #1 }
+\cs_new:Nn \@@_new:N {
+  \tl_new:N #1
+  \int_gincr:N \g_@@_register_int
+  \tl_gset:Nx #1 { \int_to_arabic:n { \g_@@_register_int } }
+  \box_new:c { \@@_box:N #1 }
+  \prop_new:c { \@@_marks:N #1 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_clear:N}
+%   The box is cleared by setting it to an empty hbox.
+%   Using \cs{box_clear:N} instead would not work because trying to push this
+%   box on the stack would not actually append any box.
+%    \begin{macrocode}
+\cs_new:Nn \@@_clear:N {
+  \hbox_set:cn { \@@_box:N #1 } {}
+  \prop_clear:c { \@@_marks:N #1 }
+  \@@_set_mark:Nnn #1 { left } { 0pt }
+  \@@_set_mark:Nnn #1 { right } { 0pt }
+  \@@_set_mark:Nnn #1 { axis } { 0pt }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Mark operations}
+%
+% \begin{macro}{\@@_set_mark:Nnn}
+%   Setting the value of a mark uses a temporary register to evaluate the
+%   dimension expression because values are stored textually in a property
+%   list.
+%    \begin{macrocode}
+\dim_new:N \l_@@_transit_dim
+\cs_new:Nn \@@_set_mark:Nnn {
+  \dim_set:Nn \l_@@_transit_dim { #3 }
+  \prop_put:cnV { \@@_marks:N #1 } { #2 }
+    \l_@@_transit_dim
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_mark:Nn}
+%   Getting the value of a mark simply consists in getting an item in a
+%   property list.
+%    \begin{macrocode}
+\cs_new:Nn \@@_mark:Nn {
+  \prop_item:cn { \@@_marks:N #1 } { #2 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_shift_x:Nn}
+%   This function shifts the marks by a specified amount, without modifying
+%   the box.
+%    \begin{macrocode}
+\cs_new:Nn \@@_shift_x:Nn {
+  \prop_map_inline:cn { \@@_marks:N #1 } {
+    \@@_set_mark:Nnn #1 { ##1 } { ##2 + #2 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_enlarge_conclusion:NN}
+%   This function moves the left and right marks of the first tree so that
+%   they are at least as far from the axis as they are in the second tree. 
+%   For instance we get the following:
+%   \begin{center}
+%     \begin{tikzpicture}[y=-3ex]
+%       \node (L1) at (1,0) {L}; \node (A1) at (2,0) {A}; \node (R1) at (4,0) {R};
+%       \node (L2) at (0,1) {L}; \node (A2) at (2,1) {A}; \node (R2) at (3,1) {R};
+%       \node (L3) at (0,2) {L}; \node (A3) at (2,2) {A}; \node (R3) at (4,2) {R};
+%       \draw (L1) -- (A1) -- (R1);
+%       \draw (L2) -- (A2) -- (R2);
+%       \draw (L3) -- (A3) -- (R3);
+%       \node[anchor=west] at (5,0) {box 1 before};
+%       \node[anchor=west] at (5,1) {box 2 before};
+%       \node[anchor=west] at (5,2) {box 1 after};
+%     \end{tikzpicture}
+%   \end{center}
+%   The contents of the trees are unchanged.
+%    \begin{macrocode}
+\cs_new:Nn \@@_enlarge_conclusion:NN {
+  \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis}
+    + \@@_mark:Nn #2 {left} - \@@_mark:Nn #2 {axis} }
+  \dim_compare:nNnT { \l_tmpa_dim } < { \@@_mark:Nn #1 {left} } {
+    \@@_set_mark:Nnn #1 {left} { \l_tmpa_dim } }
+  \dim_set:Nn \l_tmpa_dim { \@@_mark:Nn #1 {axis}
+    + \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {axis} }
+  \dim_compare:nNnT { \l_tmpa_dim } > { \@@_mark:Nn #1 {right} } {
+    \@@_set_mark:Nnn #1 {right} { \l_tmpa_dim } }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Building blocks}
+%
+% \begin{macro}{\@@_make_simple:Nn}
+%   Make a tree with explicit material in horizontal mode. Set the left and
+%   right marks to extremal positions and set the axis in the middle.
+%    \begin{macrocode}
+\cs_new:Nn \@@_make_simple:Nn {
+  \hbox_set:cn { \@@_box:N #1 } { #2 }
+  \@@_set_mark:Nnn #1 { left } { 0pt }
+  \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } / 2 }
+  \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_make_split:Nnn}
+%   Make a tree with explicit material in horizontal mode, split in two parts.
+%   Set the left and right marks to extremal positions and set the axis
+%   between the two parts.
+%    \begin{macrocode}
+\cs_new:Nn \@@_make_split:Nnn {
+  \@@_set_mark:Nnn #1 { left } { 0pt }
+  \hbox_set:cn { \@@_box:N #1 } { #2 }
+  \@@_set_mark:Nnn #1 { axis } { \box_wd:c { \@@_box:N #1 } }
+  \hbox_set:cn { \@@_box:N #1 } { \hbox_unpack:c { \@@_box:N #1 } #3 }
+  \@@_set_mark:Nnn #1 { right } { \box_wd:c { \@@_box:N #1 } }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_make_vertical:Nnnn}
+%   Make a tree with explicit material in vertical mode, using an explicit
+%   width and axis.
+%    \begin{macrocode}
+\cs_new:Nn \@@_make_vertical:Nnnn {
+  \@@_set_mark:Nnn #1 { left } { 0pt }
+  \@@_set_mark:Nnn #1 { axis } { #2 }
+  \@@_set_mark:Nnn #1 { right } { #3 }
+  \vbox_set:cn { \@@_box:N #1 } {
+    \dim_set:Nn \tex_hsize:D { \@@_mark:Nn #1 {right} }
+    #4
+  }
+  \box_set_wd:cn { \@@_box:N #1 } { \@@_mark:Nn #1 {right} }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Assembling boxes}
+%
+% \begin{macro}{\@@_extend:Nnnnn}
+%   Extend a tree box. The marks are shifted so that alignment is preserved.
+%   The arguments are dimensions for the left, top, right and bottom sides
+%   respectively.
+%    \begin{macrocode}
+\cs_new:Nn \@@_extend:Nnnnn {
+  \dim_compare:nNnF { #2 } = { 0pt } {
+    \hbox_set:cn { \@@_box:N #1 } {
+      \skip_horizontal:n { #2 }
+      \box_use:c { \@@_box:N #1 }
+    }
+    \@@_shift_x:Nn #1 { #2 }
+  }
+  \box_set_ht:Nn #1 { \box_ht:c { \@@_box:N #1 } + #3 }
+  \box_set_wd:Nn #1 { \box_wd:c { \@@_box:N #1 } + #4 }
+  \box_set_dp:Nn #1 { \box_dp:c { \@@_box:N #1 } + #5 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_append_right:NnN}
+%   Append the contents of the second tree to the first one on the right, with
+%   matching baselines. The marks of both trees are preserved. The middle
+%   argument specifies the space to insert between boxes.
+%    \begin{macrocode}
+\cs_new:Nn \@@_append_right:NnN {
+  \hbox_set:cn { \@@_box:N #1 } {
+    \box_use:c { \@@_box:N #1 }
+    \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
+    \box_use:c { \@@_box:N #3 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_append_left:NnN}
+%   Append the contents of the second tree to the first one on the left, with
+%   matching baselines. The marks of the first tree are shifted accordingly.
+%   The middle argument specifies the space to insert between boxes.
+%    \begin{macrocode}
+\cs_new:Nn \@@_append_left:NnN {
+  \@@_shift_x:Nn #1 { \box_wd:c { \@@_box:N #3 } + #2 }
+  \hbox_set:cn { \@@_box:N #1 } {
+    \box_use:c { \@@_box:N #3 }
+    \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
+    \box_use:c { \@@_box:N #1 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_align:NN}
+%   Shift one of two trees to the right so that their axes match. The marks of
+%   the one that is shifted are updated accordingly.
+%    \begin{macrocode}
+\cs_new:Nn \@@_align:NN {
+  \dim_set:Nn \l_tmpa_dim
+    { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #1 {axis} }
+  \dim_compare:nNnTF \l_tmpa_dim < { 0pt } {
+    \@@_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt }
+  } {
+    \@@_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_append_above:NN}
+%   Append the contents of the second tree above the first one, with matching
+%   axes. The marks of the first tree are preserved.
+%    \begin{macrocode}
+\cs_new:Nn \@@_append_above:NN {
+  \@@_align:NN #1 #2
+  \vbox_set:cn  { \@@_box:N #1 } {
+    \box_use:c { \@@_box:N #2 }
+    \tex_prevdepth:D -1000pt
+    \box_use:c { \@@_box:N #1 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_append_below:NN}
+%   Append the contents of the second tree below the first one, with matching
+%   axes. The marks of the first tree are preserved.
+%    \begin{macrocode}
+\cs_new:Nn \@@_append_below:NN {
+  \@@_align:NN #1 #2
+  \vbox_set_top:Nn #1 {
+    \box_use:c { \@@_box:N #1 }
+    \tex_prevdepth:D -1000pt
+    \box_use:c { \@@_box:N #2 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_overlay:NN}
+%   Append the second tree as an overlay over the first one, so that the
+%   baselines and axes match. The bounding box of the result adjusts to
+%   contain both trees.
+%    \begin{macrocode}
+\cs_new:Nn \@@_overlay:NN {
+  \@@_align:NN #1 #2
+  \hbox_set:cn { \@@_box:N #1 } {
+    \hbox_overlap_right:n { \box_use:c { \@@_box:N #1 } }
+    \box_use:c { \@@_box:N #2 }
+    \dim_compare:nNnT
+      { \box_wd:c { \@@_box:N #2 } } < { \box_wd:c { \@@_box:N #1 } }
+      { \skip_horizontal:n
+        { \box_wd:c { \@@_box:N #1 } - \box_wd:c { \@@_box:N #2 } } }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_vcenter:N}
+%   Shift the material in a tree vertically so that the height and depth are
+%   equal (like \TeX's \cs{vcenter} but around the baseline).
+%    \begin{macrocode}
+\cs_new:Nn \@@_vcenter:N {
+  \dim_set:Nn \l_tmpa_dim
+    { ( \box_ht:c { \@@_box:N #1 } - \box_dp:c { \@@_box:N #1 } ) / 2 }
+  \box_set_eq:Nc \l_tmpa_box { \@@_box:N #1 }
+  \hbox_set:cn { \@@_box:N #1 }
+    { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsection{Making inferences}
+%
+% The following commands use the parameters defined at the beginning of the
+% package for actually building proof trees using the commands defined above.
+%
+% \begin{macro}{\@@_append_vertical:NN}
+%   Append the contents of the second tree above or below the first one,
+%   depending on current settings. Axes are aligned and the marks of the first
+%   tree are preserved.
+%    \begin{macrocode}
+\cs_new:Nn \@@_append_vertical:NN {
+  \bool_if:NTF \l_@@_updown_bool
+    { \@@_append_below:NN #1 #2 }
+    { \@@_append_above:NN #1 #2 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_make_rule_for:NNN}
+%   Make a box containing an inference rule with labels, using the current
+%   settings. The width and axis position are taken as those of the conclusion
+%   of another tree box. The third argument is used as a temporary register
+%   for building labels.
+%    \begin{macrocode}
+\cs_new:Nn \@@_make_rule_for:NNN {
+%    \end{macrocode}
+%   Build the rule.
+%    \begin{macrocode}
+  \@@_make_vertical:Nnnn #1
+    { \@@_mark:Nn #2 {axis} - \@@_mark:Nn #2 {left} }
+    { \@@_mark:Nn #2 {right} - \@@_mark:Nn #2 {left} }
+    {
+      \skip_vertical:N \l_@@_rule_margin_dim
+      \tl_if_empty:NF { \l_@@_rule_code_tl } {
+        \tl_use:N \l_@@_rule_code_tl
+        \skip_vertical:N \l_@@_rule_margin_dim
+      }
+    }
+  \@@_vcenter:N #1
+%    \end{macrocode}
+%   Append the left label.
+%    \begin{macrocode}
+  \tl_if_blank:VF \l_@@_left_label_tl {
+    \@@_make_simple:Nn #3 {
+      \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n {
+        \cs_set_eq:NN \inserttext \l_@@_left_label_tl
+        \tl_use:N \l_@@_left_label_template_tl
+      } }
+    }
+    \box_set_ht:cn { \@@_box:N #3 } { 0pt }
+    \box_set_dp:cn { \@@_box:N #3 } { 0pt }
+    \@@_append_left:NnN
+      \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box
+  }
+%    \end{macrocode}
+%   Append the right label.
+%    \begin{macrocode}
+  \tl_if_blank:VF \l_@@_right_label_tl {
+    \@@_make_simple:Nn #3 {
+      \box_move_down:nn { \l_@@_label_axis_dim } { \hbox:n {
+        \cs_set_eq:NN \inserttext \l_@@_right_label_tl
+        \tl_use:N \l_@@_right_label_template_tl
+      } }
+    }
+    \box_set_ht:cn { \@@_box:N #3 } { 0pt }
+    \box_set_dp:cn { \@@_box:N #3 } { 0pt }
+    \@@_append_right:NnN
+      \l_@@_c_box \l_@@_label_separation_dim \l_@@_d_box
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsection{Stack-based interface}
+%
+% \subsubsection{The stack}
+%
+% Logically, box structures are stored on a stack. However, \TeX\ does not
+% provide data structures for that and the grouping mechanism is not flexible
+% enough, so we encode them using what we actually have. A stack for boxes is
+% implemented using a global hbox \cs{g_@@_stack_box} that contains all the
+% boxes successively. A sequence \cs{g_@@_stack_seq} is used to store the
+% dimensions property lists textually. We maintain a counter
+% \cs{g_@@_level_int} with the number of elements on the stack, for
+% consistency checks.
+%    \begin{macrocode}
+\int_new:N \g_@@_level_int
+\box_new:N \g_@@_stack_box
+\seq_new:N \g_@@_stack_seq
+%    \end{macrocode}
+%
+% \begin{macro}{\@@_clear_stack:}
+%   Clear the stack.
+%    \begin{macrocode}
+\cs_new:Nn \@@_clear_stack: {
+  \int_gset:Nn \g_@@_level_int { 0 }
+  \hbox_gset:Nn \g_@@_stack_box { }
+  \seq_gclear:N \g_@@_stack_seq
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_push:N}
+%   Push the contents of a register on the stack.
+%    \begin{macrocode}
+\cs_new:Nn \@@_push:N {
+  \int_gincr:N \g_@@_level_int
+  \hbox_gset:Nn \g_@@_stack_box
+    { \hbox_unpack:N \g_@@_stack_box \box_use:c { \@@_box:N #1 } }
+  \seq_gput_left:Nv \g_@@_stack_seq
+    { \@@_marks:N #1 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_pop:N}
+%   Pop the value from the top of the stack into a register.
+%    \begin{macrocode}
+\cs_new:Nn \@@_pop:N {
+  \int_compare:nNnTF { \g_@@_level_int } > { 0 } {
+    \int_gdecr:N \g_@@_level_int
+    \hbox_gset:Nn \g_@@_stack_box {
+      \hbox_unpack:N \g_@@_stack_box
+      \box_gset_to_last:N \g_tmpa_box
+    }
+    \box_set_eq_clear:cN { \@@_box:N #1 } \g_tmpa_box
+    \seq_gpop_left:NN \g_@@_stack_seq \l_tmpa_tl
+    \tl_set_eq:cN { \@@_marks:N #1 } \l_tmpa_tl
+  } {
+    \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{}
+    \@@_clear:N #1
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Assembling trees}
+%
+%    \begin{macrocode}
+\@@_new:N \l_@@_a_box
+\@@_new:N \l_@@_b_box
+\@@_new:N \l_@@_c_box
+\@@_new:N \l_@@_d_box
+%    \end{macrocode}
+%
+% \begin{macro}{\@@_join_horizontal:n}
+%   Join horizontally a number of elements at the top of the stack. If several
+%   trees are joined, use the left mark of the left tree, the right mark of
+%   the right tree and set the axis in the middle of these marks.
+%    \begin{macrocode}
+\cs_new:Nn \@@_join_horizontal:n {
+  \int_case:nnF { #1 } {
+  { 0 } {
+    \group_begin:
+    \@@_clear:N \l_@@_a_box
+    \@@_push:N \l_@@_a_box
+    \group_end:
+  }
+  { 1 } { }
+  } {
+    \group_begin:
+    \@@_pop:N \l_@@_a_box
+    \prg_replicate:nn { #1 - 1 } {
+      \@@_pop:N \l_@@_b_box
+      \@@_append_left:NnN
+        \l_@@_a_box \l_@@_separation_dim \l_@@_b_box
+    }
+    \@@_set_mark:Nnn \l_@@_a_box { left }
+      { \@@_mark:Nn \l_@@_b_box { left } }
+    \@@_set_mark:Nnn \l_@@_a_box { axis }
+      { ( \@@_mark:Nn \l_@@_a_box { left }
+        + \@@_mark:Nn \l_@@_a_box { right } ) / 2 }
+    \@@_push:N \l_@@_a_box
+    \group_end:
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_join_vertical:}
+%   Join vertically the two elements at the top of the stack, with a
+%   horizontal rule of the appropriate size.
+%    \begin{macrocode}
+\cs_new:Nn \@@_join_vertical: {
+  \group_begin:
+  \@@_pop:N \l_@@_a_box
+  \@@_pop:N \l_@@_b_box
+  \@@_enlarge_conclusion:NN \l_@@_b_box \l_@@_a_box
+  \@@_make_rule_for:NNN \l_@@_c_box \l_@@_b_box
+    \l_@@_d_box
+  \@@_append_vertical:NN \l_@@_a_box \l_@@_c_box
+  \@@_append_vertical:NN \l_@@_a_box \l_@@_b_box
+  \@@_push:N \l_@@_a_box
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{High-level commands}
+%
+% \begin{macro}{\@@_statement_parse:w}
+%   An auxiliary function for parsing the argument in
+%   \cs{@@_push_statement:n}.
+%    \begin{macrocode}
+\cs_new:Npn \@@_statement_parse:w #1 & #2 & #3 \q_stop {
+  \tl_if_empty:nTF { #3 } {
+    \@@_make_simple:Nn \l_@@_a_box
+      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_template_tl }
+  } {
+    \@@_make_split:Nnn \l_@@_a_box
+      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_@@_left_template_tl }
+      { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_@@_right_template_tl }
+  }
+  \@@_push:N \l_@@_a_box
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_push_statement:n}
+%   Push a box with default formatting, using explicit alignment if the code
+%   contains a |&| character
+%    \begin{macrocode}
+\cs_new:Nn \@@_push_statement:n {
+  \@@_statement_parse:w #1 & & \q_stop
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsection{Document interface}
+%
+% \subsubsection{Functions to define statements}
+%
+% The \cs{g_@@_statements_seq} variable contains the list of all defined
+% statements. For each statement |X|, there is a document command \cs{ebproofX}
+% and the alias \cs{X} is defined when entering a |prooftree| environment.
+%    \begin{macrocode}
+\seq_new:N \g_@@_statements_seq
+%    \end{macrocode}
+%
+% \begin{macro}{\@@_setup_statements:}
+%   Install the aliases for statements, saving the original value of the control
+%   sequences.
+%    \begin{macrocode}
+\cs_new:Nn \@@_setup_statements: {
+  \seq_map_inline:Nn \g_@@_statements_seq {
+    \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 }
+    \cs_set_eq:cc { ##1 } { ebproof ##1 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_restore_statements:}
+%   Restore the saved meanings of the control sequences. This is useful when
+%   interpreting user-provided code in statement arguments. The meanings are
+%   automatically restored when leaving a |prooftree| environment because of
+%   grouping.
+%    \begin{macrocode}
+\cs_new:Nn \@@_restore_statements: {
+  \seq_map_inline:Nn \g_@@_statements_seq {
+    \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 }
+  }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_new_statement:nnn}
+%   Define a new statement. The first argument is the name, the second one is
+%   an argument specifier as used by |xparse| and the third one is the body of
+%   the command.
+%    \begin{macrocode}
+\cs_new:Nn \@@_new_statement:nnn {
+  \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 }
+  \seq_put_right:Nn \g_@@_statements_seq { #1 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\@@_new_deprecated_statement:nnnn}
+%   Define a deprecated statement. The syntax is the same as above except that
+%   an extra argument in third position indicates what should be used instead.
+%   The effect is the same except that a warning message is issued the first
+%   time the statement is used.
+%    \begin{macrocode}
+\cs_new:Nn \@@_new_deprecated_statement:nnnn {
+  \cs_new:cpn { ebproof_#1_warning: } {
+    \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 }
+    \cs_gset:cn { ebproof_#1_warning: } { }
+  }
+  \@@_new_statement:nnn { #1 } { #2 }
+    { \use:c { ebproof_#1_warning: } #4 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+%
+% \subsubsection{Basic commands}
+%
+% \begin{macro}{\ebproofset,\set}
+%   This is a simple wrapper around \cs{keys_set:nn}.
+%    \begin{macrocode}
+\@@_new_statement:nnn { set } { m } {
+  \keys_set:nn { ebproof } { #1 }
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\hypo}
+%   This is mostly a wrapper around \cs{ebproof_push_statement:n}, with
+%   material to handle options and the statements macros.
+%    \begin{macrocode}
+\@@_new_statement:nnn { hypo } { O{} m } {
+  \group_begin:
+  \@@_restore_statements:
+  \keys_set:nn { ebproof } { #1 }
+  \@@_push_statement:n { #2 }
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\infer}
+%   This is a bit more involved than \cs{hypo} because we have to handle rule
+%   style options and joining.
+%    \begin{macrocode}
+\@@_new_statement:nnn { infer } { O{} m O{} m } {
+  \group_begin:
+  \@@_restore_statements:
+  \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl
+  \keys_set:nV { ebproof } \l_tmpa_tl
+  \tl_set:Nn \l_@@_right_label_tl { #3 }
+  \@@_join_horizontal:n { #2 }
+  \@@_push_statement:n { #4 }
+  \@@_join_vertical:
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\ellipsis}
+%   An ellipsis is made by hand using vertical leaders to render the dots
+%   after rendering the label.
+%    \begin{macrocode}
+\@@_new_statement:nnn { ellipsis } { m m } {
+  \group_begin:
+  \@@_restore_statements:
+  \tl_clear:N \l_@@_rule_code_tl
+  \@@_make_split:Nnn \l_@@_a_box { } {
+    \vbox_set:Nn \l_tmpa_box {
+      \skip_vertical:n { 1.2ex }
+      \hbox:n { \tex_ignorespaces:D #1 }
+      \skip_vertical:n { 1.2ex }
+    }
+    \vbox_to_ht:nn { \box_ht:N \l_tmpa_box } {
+      \tex_xleaders:D \vbox_to_ht:nn { .8ex }
+        { \tex_vss:D \hbox:n { . } \tex_vss:D }
+      \tex_vfill:D
+    }
+    \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box }
+  }
+  \@@_push:N \l_@@_a_box
+  \@@_join_vertical:
+  \@@_push_statement:n {#2}
+  \@@_join_vertical:
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Modifying trees}
+%
+% \begin{macro}{\rewrite}
+%   Rewrite the box at the top of the stack while preserving its dimensions an
+%   marks. The code is typeset in horizontal mode, with control sequences to
+%   access the original box and its marks.
+%    \begin{macrocode}
+\@@_new_statement:nnn { rewrite } { m } {
+  \group_begin:
+  \@@_restore_statements:
+  \@@_pop:N \l_@@_a_box
+  \box_set_eq:Nc \l_tmpa_box { \@@_box:N \l_@@_a_box }
+  \hbox_set:Nn \l_tmpb_box {
+    \cs_set_eq:NN \treebox \l_tmpa_box
+    \cs_set:Npn \treemark { \@@_mark:Nn \l_@@_a_box }
+    { #1 }
+  }
+  \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \@@_box:N \l_@@_a_box } }
+  \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \@@_box:N \l_@@_a_box } }
+  \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \@@_box:N \l_@@_a_box } }
+  \box_set_eq:cN { \@@_box:N \l_@@_a_box } \l_tmpb_box
+  \@@_push:N \l_@@_a_box
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\delims}
+%   Insert \cs{left} and \cs{right} delimiters without changing the alignment.
+%    \begin{macrocode}
+\@@_new_statement:nnn { delims } { m m } {
+  \group_begin:
+  \@@_restore_statements:
+  \@@_pop:N \l_@@_a_box
+  \hbox_set:Nn \l_tmpa_box
+    { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ }
+  \dim_set:Nn \l_tmpa_dim
+    { \box_ht:N \l_tmpa_box - \box_ht:c { \@@_box:N \l_@@_a_box } }
+  \hbox_set:cn { \@@_box:N \l_@@_a_box } {
+    $ #1 \tex_vrule:D
+      height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt
+    \tex_right:D . $
+  }
+  \@@_shift_x:Nn \l_@@_a_box
+    { \box_wd:c { \@@_box:N \l_@@_a_box } }
+  \hbox_set:cn { \@@_box:N \l_@@_a_box } {
+    \hbox_unpack:c { \@@_box:N \l_@@_a_box }
+    $ \tex_left:D . \box_use:N \l_tmpa_box #2 $
+  }
+  \hbox_set:cn { \@@_box:N \l_@@_a_box }
+    { \box_move_down:nn { \l_tmpa_dim }
+        { \box_use:c { \@@_box:N \l_@@_a_box } } }
+  \@@_push:N \l_@@_a_box
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\overlay}
+%   Pop two trees and append the second tree as an overlay over the first one,
+%   so that the baselines and axes match. The bounding box of the result
+%   adjusts to contain both trees.
+%    \begin{macrocode}
+\@@_new_statement:nnn { overlay } { } {
+  \group_begin:
+  \@@_pop:N \l_@@_a_box
+  \@@_pop:N \l_@@_b_box
+  \@@_overlay:NN \l_@@_a_box \l_@@_b_box
+  \@@_push:N \l_@@_a_box
+  \group_end:
+}
+%    \end{macrocode}
+% \end{macro}
+%
+% \subsubsection{Deprecated statements}
+%
+% These statements were defined in versions 1.x of the package, they are
+% preserved for temporary upwards compatibility and will be removed in a
+% future version.
+%    \begin{macrocode}
+\@@_new_deprecated_statement:nnnn { Alter } { m }
+  { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } }
+\@@_new_deprecated_statement:nnnn { Delims } { }
+  { use~\token_to_str:c{delims}~instead } { \ebproofdelims }
+\@@_new_deprecated_statement:nnnn { Ellipsis } { }
+  { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis }
+\@@_new_deprecated_statement:nnnn { Hypo } { }
+  { use~\token_to_str:c{hypo}~instead } { \ebproofhypo }
+\@@_new_deprecated_statement:nnnn { Infer } { }
+  { use~\token_to_str:c{infer}~instead } { \ebproofinfer }
+%    \end{macrocode}
+%
+%
+% \subsubsection{Environment interface}
+%
+% The stack is initialised globally. The \env{prooftree} environment does not
+% clear the stack, instead it saves the initial level in order to check that
+% statements are properly balanced. This allows for nested uses of the
+% environment, if it ever happens to be useful.
+%
+%    \begin{macrocode}
+\@@_clear_stack:
+\tl_new:N \l_@@_start_level_tl
+%    \end{macrocode}
+%
+% \begin{macro}{prooftree,prooftree*}
+%   The \env{prooftree} environment.
+%    \begin{macrocode}
+\NewDocumentEnvironment { prooftree } { s O{} } {
+  \group_align_safe_begin:
+  \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl
+  \keys_set:nV { ebproof } \l_tmpa_tl
+  \tl_set:Nx \l_@@_start_level_tl { \int_use:N \g_@@_level_int }
+  \vbox_set:Nw \l_tmpa_box
+  \@@_setup_statements:
+} {
+  \vbox_set_end:
+  \@@_pop:N \l_@@_a_box
+  \int_compare:nNnF { \g_@@_level_int } = { \tl_use:N \l_@@_start_level_tl } {
+    \PackageError{ebproof}{Malformed~proof~tree}{
+      Some~hypotheses~were~declared~but~not~used~in~this~tree.}
+  }
+  \IfBooleanTF { #1 } {
+    \[ \box_use:c { \@@_box:N \l_@@_a_box } \]
+    \ignorespacesafterend
+  } {
+    \hbox_unpack:N \c_empty_box
+    \bool_if:NTF \l_@@_center_bool {
+      \hbox:n { $ \tex_vcenter:D { \box_use:c { \@@_box:N \l_@@_a_box } } $ }
+    } {
+      \box_use:c { \@@_box:N \l_@@_a_box }
+    }
+  }
+  \group_align_safe_end:
+}
+%    \end{macrocode}
+% A trick for the starred version:
+%    \begin{macrocode}
+\cs_new:cpn { prooftree* } { \prooftree* }
+\cs_new:cpn { endprooftree* } { \endprooftree }
+%    \end{macrocode}
+% \end{macro}
+%
+%    \begin{macrocode}
+%</package>
+%    \end{macrocode}
+%
+% \end{implementation}
diff --git a/Master/texmf-dist/source/latex/ebproof/ebproof.ins b/Master/texmf-dist/source/latex/ebproof/ebproof.ins
new file mode 100644
index 00000000000..25bcc734965
--- /dev/null
+++ b/Master/texmf-dist/source/latex/ebproof/ebproof.ins
@@ -0,0 +1,15 @@
+%% Copyright (C) 2015-2018 by Emmanuel Beffara
+%%
+%% This file may be distributed and/or modified under the conditions of the
+%% LaTeX Project Public License, either version 1.3 of this license or (at
+%% your option) any later version. The latest version of this license is in:
+%% 
+%%   http://www.latex-project.org/lppl.txt
+%% 
+%% and version 1.3 or later is part of all distributions of LaTeX version
+%% 2005/12/01 or later.
+
+\input l3docstrip.tex
+\keepsilent \askforoverwritefalse
+\generate{\file{ebproof.sty}{\from{ebproof.dtx}{package}}}
+\endbatchfile
diff --git a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
index 7601f8e9e85..c2d1d0812e7 100644
--- a/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
+++ b/Master/texmf-dist/tex/latex/ebproof/ebproof.sty
@@ -1,117 +1,86 @@
-% The ebproof package - Formal proofs in the style of sequent calculus
-
-%% ebproof.sty
-%% Copyright 2017 Emmanuel Beffara <manu@beffara.org>
-
-% This work may be distributed and/or modified under the
-% conditions of the LaTeX Project Public License, either version 1.3
-% of this license or (at your option) any later version.
-% The latest version of this license is in
-%   http://www.latex-project.org/lppl.txt
-% and version 1.3 or later is part of all distributions of LaTeX
-% version 2005/12/01 or later.
-
-% This work has the LPPL maintenance status `maintained'.
-
-% The Current Maintainer of this work is Emmanuel Beffara.
-
-% This work consists of the files ebproof.sty and ebproof.tex.
-
+%%
+%% This is file `ebproof.sty',
+%% generated with the docstrip utility.
+%%
+%% The original source files were:
+%%
+%% ebproof.dtx  (with options: `package')
+%% 
+%% IMPORTANT NOTICE:
+%% 
+%% For the copyright see the source file.
+%% 
+%% Any modified versions of this file must be renamed
+%% with new filenames distinct from ebproof.sty.
+%% 
+%% For distribution of the original source see the terms
+%% for copying and modification in the file ebproof.dtx.
+%% 
+%% This generated file may be distributed as long as the
+%% original source files, as listed above, are part of the
+%% same distribution. (The sources need not necessarily be
+%% in the same archive or directory.)
 \NeedsTeXFormat{LaTeX2e}
 \RequirePackage{expl3}
 \RequirePackage{xparse}
-\ProvidesExplPackage{ebproof}{2017/05/17}{2.0}{EB's proof trees}
-
-
-%% Parameters
-
-%%% Declaration of the parameters
-
+\ProvidesExplPackage{ebproof}{2020/08/19}{2.1}{EB's proof trees}
 \keys_define:nn { ebproof } {
-
-% general shape
-
-center .bool_set:N = \l_ebproof_center_bool,
-
+center .bool_set:N = \l__ebproof_center_bool,
 proof~style .choice: ,
-proof~style / upwards .code:n = \bool_set_false:N \l_ebproof_updown_bool,
-proof~style / downwards .code:n = \bool_set_true:N \l_ebproof_updown_bool,
-
-% spacing
-
-separation .dim_set:N = \l_ebproof_separation_dim,
-rule~margin .dim_set:N = \l_ebproof_rule_margin_dim,
-
-% shape of inference lines
-
-rule~thickness .dim_set:N = \l_ebproof_rule_thickness_dim,
-rule~separation .dim_set:N = \l_ebproof_rule_separation_dim,
-rule~dash~length .dim_set:N = \l_ebproof_rule_dash_length_dim,
-rule~dash~space .dim_set:N = \l_ebproof_rule_dash_space_dim,
-rule~code .tl_set:N = \l_ebproof_rule_code_tl,
-
+proof~style / upwards .code:n = \bool_set_false:N \l__ebproof_updown_bool,
+proof~style / downwards .code:n = \bool_set_true:N \l__ebproof_updown_bool,
+separation .dim_set:N = \l__ebproof_separation_dim,
+rule~margin .dim_set:N = \l__ebproof_rule_margin_dim,
+rule~thickness .dim_set:N = \l__ebproof_rule_thickness_dim,
+rule~separation .dim_set:N = \l__ebproof_rule_separation_dim,
+rule~dash~length .dim_set:N = \l__ebproof_rule_dash_length_dim,
+rule~dash~space .dim_set:N = \l__ebproof_rule_dash_space_dim,
+rule~code .tl_set:N = \l__ebproof_rule_code_tl,
 rule~style .choice:,
-
-% templates
-
-template .tl_set:N = \l_ebproof_template_tl,
-left~template .tl_set:N = \l_ebproof_left_template_tl,
-right~template .tl_set:N = \l_ebproof_right_template_tl,
-
-% labels
-
-left~label .tl_set:N = \l_ebproof_left_label_tl,
-right~label .tl_set:N = \l_ebproof_right_label_tl,
-left~label~template .tl_set:N = \l_ebproof_left_label_template_tl,
-right~label~template .tl_set:N = \l_ebproof_right_label_template_tl,
-label~separation .dim_set:N = \l_ebproof_label_separation_dim,
-label~axis .dim_set:N = \l_ebproof_label_axis_dim,
-
-}
-
-%%% Rule styles
-
+template .tl_set:N = \l__ebproof_template_tl,
+left~template .tl_set:N = \l__ebproof_left_template_tl,
+right~template .tl_set:N = \l__ebproof_right_template_tl,
+left~label .tl_set:N = \l__ebproof_left_label_tl,
+right~label .tl_set:N = \l__ebproof_right_label_tl,
+left~label~template .tl_set:N = \l__ebproof_left_label_template_tl,
+right~label~template .tl_set:N = \l__ebproof_right_label_template_tl,
+label~separation .dim_set:N = \l__ebproof_label_separation_dim,
+label~axis .dim_set:N = \l__ebproof_label_axis_dim,
+}
 \NewDocumentCommand \ebproofnewrulestyle { mm } {
   \keys_define:nn { ebproof } {
     rule~style / #1 .meta:nn = { ebproof } { #2 }
   }
 }
-
 \ebproofnewrulestyle { simple } {
-  rule~code = { \tex_hrule:D height \l_ebproof_rule_thickness_dim }
+  rule~code = { \tex_hrule:D height \l__ebproof_rule_thickness_dim }
 }
-
 \ebproofnewrulestyle { no~rule } {
   rule~code =
 }
-
 \ebproofnewrulestyle { double } {
   rule~code = {
-    \tex_hrule:D height \l_ebproof_rule_thickness_dim
-    \skip_vertical:N \l_ebproof_rule_separation_dim
-    \tex_hrule:D height \l_ebproof_rule_thickness_dim
+    \tex_hrule:D height \l__ebproof_rule_thickness_dim
+    \skip_vertical:N \l__ebproof_rule_separation_dim
+    \tex_hrule:D height \l__ebproof_rule_thickness_dim
   }
 }
-
 \ebproofnewrulestyle { dashed } {
   rule~code = {
     \hbox_to_wd:nn { \tex_hsize:D } {
-      \dim_set:Nn \l_tmpa_dim { \l_ebproof_rule_dash_space_dim / 2 }
+      \dim_set:Nn \l_tmpa_dim { \l__ebproof_rule_dash_space_dim / 2 }
       \skip_horizontal:n { -\l_tmpa_dim }
       \tex_cleaders:D \hbox:n {
         \skip_horizontal:N \l_tmpa_dim
         \tex_vrule:D
-          height \l_ebproof_rule_thickness_dim
-          width \l_ebproof_rule_dash_length_dim
+          height \l__ebproof_rule_thickness_dim
+          width \l__ebproof_rule_dash_length_dim
         \skip_horizontal:N \l_tmpa_dim
-      }\tex_hfill:D
+      } \tex_hfill:D
       \skip_horizontal:n { -\l_tmpa_dim }
     }
   }
 }
-
-%%% Default values
-
 \keys_set:nn { ebproof } {
   center = true,
   proof~style = upwards,
@@ -132,513 +101,321 @@ label~axis .dim_set:N = \l_ebproof_label_axis_dim,
   label~separation = 0.5em,
   label~axis = 0.5ex
 }
-
-%%% Defining style macros
-
 \NewDocumentCommand \ebproofnewstyle { mm } {
   \keys_define:nn { ebproof } { #1 .meta:n = { #2 } }
 }
-
-
-%% Proof trees
-
-% Proof trees are represented as a data structure that consists of a box and a
-% set of marks, which are vertical positions in the box (as distances from the
-% left edge). Arbitrary marks can be defined, the folowing are used for
-% alignment:
-% - left :  the left of the conclusion
-% - right : the right of the conclusion
-% - axis :  the vertical axis of the conclusion
-
-
-%%% Registers
-
-% TeX does not actually provide data structures, so we have to encode things.
-% We provide an allocator for "registers" holding boxes with attributes. Such
-% a register consists in a box register and a property list for marks, which
-% maps mark names to values as explicit dimensions with units.
-
-% Create a new register.
-
-\cs_new:Nn \ebproof_new:N {
-  \box_new:N #1
-  \prop_new:c { l_ebproof_marks_ \__int_value:w #1 _prop }
-}
-
-% Clear a register.
-
-\cs_new:Nn \ebproof_clear:N {
-  \hbox_set:Nn #1 {}
-  % Using \box_clear:N instead would not work because trying to push this box
-  % on the stack would not actually append any box.
-  \prop_clear:c { l_ebproof_marks_ \__int_value:w #1 _prop }
-  \ebproof_set_mark:Nnn #1 { left } { 0pt }
-  \ebproof_set_mark:Nnn #1 { right } { 0pt }
-  \ebproof_set_mark:Nnn #1 { axis } { 0pt }
-}
-
-
-%%% Mark operations
-
-% Set the value of a mark. The third argument is a dimension expression.
-
-\dim_new:N \l_ebproof_transit_dim
-
-\cs_new:Nn \ebproof_set_mark:Nnn {
-  \dim_set:Nn \l_ebproof_transit_dim { #3 }
-  \prop_put:cnV { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 }
-    \l_ebproof_transit_dim
-}
-
-% Get the value of a mark. This is expandable and can be used in expressions.
-
-\cs_new:Nn \ebproof_mark:Nn {
-  \prop_item:cn { l_ebproof_marks_ \__int_value:w #1 _prop } { #2 }
-}
-
-% Shift the marks by a specified amount, without modifying the box.
-
-\cs_new:Nn \ebproof_shift_x:Nn {
-  \prop_map_inline:cn { l_ebproof_marks_ \__int_value:w #1 _prop } {
-    \ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 }
+\int_new:N \g__ebproof_register_int
+\cs_new:Nn \__ebproof_box:N { g__ebproof_box_ \tl_use:N #1 }
+\cs_new:Nn \__ebproof_marks:N { g__ebproof_marks_ \tl_use:N #1 }
+\cs_new:Nn \__ebproof_new:N {
+  \tl_new:N #1
+  \int_gincr:N \g__ebproof_register_int
+  \tl_gset:Nx #1 { \int_to_arabic:n { \g__ebproof_register_int } }
+  \box_new:c { \__ebproof_box:N #1 }
+  \prop_new:c { \__ebproof_marks:N #1 }
+}
+\cs_new:Nn \__ebproof_clear:N {
+  \hbox_set:cn { \__ebproof_box:N #1 } {}
+  \prop_clear:c { \__ebproof_marks:N #1 }
+  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
+  \__ebproof_set_mark:Nnn #1 { right } { 0pt }
+  \__ebproof_set_mark:Nnn #1 { axis } { 0pt }
+}
+\dim_new:N \l__ebproof_transit_dim
+\cs_new:Nn \__ebproof_set_mark:Nnn {
+  \dim_set:Nn \l__ebproof_transit_dim { #3 }
+  \prop_put:cnV { \__ebproof_marks:N #1 } { #2 }
+    \l__ebproof_transit_dim
+}
+\cs_new:Nn \__ebproof_mark:Nn {
+  \prop_item:cn { \__ebproof_marks:N #1 } { #2 }
+}
+\cs_new:Nn \__ebproof_shift_x:Nn {
+  \prop_map_inline:cn { \__ebproof_marks:N #1 } {
+    \__ebproof_set_mark:Nnn #1 { ##1 } { ##2 + #2 }
   }
 }
-
-% Move the left and right marks of the first tree so that they are at least as
-% far from the axis as they are in the second tree. For instance if the marks
-% are set as
-%    1:      L---A-------R
-%    2:  L-------A---R
-% then the marks of the first tree are then set as
-%    1:  L-------A-------R
-% The contents of the tree are unchanged.
-
-\cs_new:Nn \ebproof_enlarge_conclusion:NN {
-  \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis}
-    + \ebproof_mark:Nn #2 {left} - \ebproof_mark:Nn #2 {axis} }
-  \dim_compare:nNnT { \l_tmpa_dim } < { \ebproof_mark:Nn #1 {left} } {
-    \ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } }
-  \dim_set:Nn \l_tmpa_dim { \ebproof_mark:Nn #1 {axis}
-    + \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {axis} }
-  \dim_compare:nNnT { \l_tmpa_dim } > { \ebproof_mark:Nn #1 {right} } {
-    \ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } }
-}
-
-
-%%% Building blocks
-
-% Make a tree with explicit material in horizontal mode. Set the left and
-% right marks to extremal positions and set the axis in the middle.
-
-\cs_new:Nn \ebproof_make_simple:Nn {
-  \hbox_set:Nn #1 { #2 }
-  \ebproof_set_mark:Nnn #1 { left } { 0pt }
-  \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 / 2 }
-  \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 }
-}
-
-% Make a tree with explicit material in horizontal mode, split in two parts.
-% Set the left and right marks to extremal positions and set the axis between
-% the two parts.
-
-\cs_new:Nn \ebproof_make_split:Nnn {
-  \ebproof_set_mark:Nnn #1 { left } { 0pt }
-  \hbox_set:Nn #1 { #2 }
-  \ebproof_set_mark:Nnn #1 { axis } { \box_wd:N #1 }
-  \hbox_set:Nn #1 { \hbox_unpack:N #1 #3 }
-  \ebproof_set_mark:Nnn #1 { right } { \box_wd:N #1 }
-}
-
-% Make a tree with explicit material in vertical mode, using an explicit width
-% and axis.
-
-\cs_new:Nn \ebproof_make_vertical:Nnnn {
-  \ebproof_set_mark:Nnn #1 { left } { 0pt }
-  \ebproof_set_mark:Nnn #1 { axis } { #2 }
-  \ebproof_set_mark:Nnn #1 { right } { #3 }
-  \vbox_set:Nn #1 {
-    \dim_set:Nn \tex_hsize:D { \ebproof_mark:Nn #1 {right} }
+\cs_new:Nn \__ebproof_enlarge_conclusion:NN {
+  \dim_set:Nn \l_tmpa_dim { \__ebproof_mark:Nn #1 {axis}
+    + \__ebproof_mark:Nn #2 {left} - \__ebproof_mark:Nn #2 {axis} }
+  \dim_compare:nNnT { \l_tmpa_dim } < { \__ebproof_mark:Nn #1 {left} } {
+    \__ebproof_set_mark:Nnn #1 {left} { \l_tmpa_dim } }
+  \dim_set:Nn \l_tmpa_dim { \__ebproof_mark:Nn #1 {axis}
+    + \__ebproof_mark:Nn #2 {right} - \__ebproof_mark:Nn #2 {axis} }
+  \dim_compare:nNnT { \l_tmpa_dim } > { \__ebproof_mark:Nn #1 {right} } {
+    \__ebproof_set_mark:Nnn #1 {right} { \l_tmpa_dim } }
+}
+\cs_new:Nn \__ebproof_make_simple:Nn {
+  \hbox_set:cn { \__ebproof_box:N #1 } { #2 }
+  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
+  \__ebproof_set_mark:Nnn #1 { axis } { \box_wd:c { \__ebproof_box:N #1 } / 2 }
+  \__ebproof_set_mark:Nnn #1 { right } { \box_wd:c { \__ebproof_box:N #1 } }
+}
+\cs_new:Nn \__ebproof_make_split:Nnn {
+  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
+  \hbox_set:cn { \__ebproof_box:N #1 } { #2 }
+  \__ebproof_set_mark:Nnn #1 { axis } { \box_wd:c { \__ebproof_box:N #1 } }
+  \hbox_set:cn { \__ebproof_box:N #1 } { \hbox_unpack:c { \__ebproof_box:N #1 } #3 }
+  \__ebproof_set_mark:Nnn #1 { right } { \box_wd:c { \__ebproof_box:N #1 } }
+}
+\cs_new:Nn \__ebproof_make_vertical:Nnnn {
+  \__ebproof_set_mark:Nnn #1 { left } { 0pt }
+  \__ebproof_set_mark:Nnn #1 { axis } { #2 }
+  \__ebproof_set_mark:Nnn #1 { right } { #3 }
+  \vbox_set:cn { \__ebproof_box:N #1 } {
+    \dim_set:Nn \tex_hsize:D { \__ebproof_mark:Nn #1 {right} }
     #4
   }
-  \box_set_wd:Nn #1 { \ebproof_mark:Nn #1 {right} }
-}
-
-%%% Assembling boxes
-
-% Extend a tree box. The marks are shifted so that alignment is preserved. The
-% arguments are dimensions for the left, top, right and bottom sides
-% respectively.
-
-\cs_new:Nn \ebproof_extend:Nnnnn {
+  \box_set_wd:cn { \__ebproof_box:N #1 } { \__ebproof_mark:Nn #1 {right} }
+}
+\cs_new:Nn \__ebproof_extend:Nnnnn {
   \dim_compare:nNnF { #2 } = { 0pt } {
-    \hbox_set:Nn #1 {
+    \hbox_set:cn { \__ebproof_box:N #1 } {
       \skip_horizontal:n { #2 }
-      \box_use:N #1
+      \box_use:c { \__ebproof_box:N #1 }
     }
-    \ebproof_shift_x:Nn #1 { #2 }
+    \__ebproof_shift_x:Nn #1 { #2 }
   }
-  \box_set_ht:Nn #1 { \box_ht:N #1 + #3 }
-  \box_set_wd:Nn #1 { \box_wd:N #1 + #4 }
-  \box_set_dp:Nn #1 { \box_dp:N #1 + #5 }
-}
-
-% Append the contents of the second tree to the first one on the right, with
-% matching baselines. The marks of both trees are preserved. The middle
-% argument specifies the space to insert between boxes.
-
-\cs_new:Nn \ebproof_append_right:NnN {
-  \hbox_set:Nn #1 {
-    \box_use:N #1
+  \box_set_ht:Nn #1 { \box_ht:c { \__ebproof_box:N #1 } + #3 }
+  \box_set_wd:Nn #1 { \box_wd:c { \__ebproof_box:N #1 } + #4 }
+  \box_set_dp:Nn #1 { \box_dp:c { \__ebproof_box:N #1 } + #5 }
+}
+\cs_new:Nn \__ebproof_append_right:NnN {
+  \hbox_set:cn { \__ebproof_box:N #1 } {
+    \box_use:c { \__ebproof_box:N #1 }
     \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
-    \box_use:N #3
+    \box_use:c { \__ebproof_box:N #3 }
   }
 }
-
-% Append the contents of the second tree to the first one on the left, with
-% matching baselines. The marks of the first tree are shifted accordingly. The
-% middle argument specifies the space to insert between boxes.
-
-\cs_new:Nn \ebproof_append_left:NnN {
-  \ebproof_shift_x:Nn #1 { \box_wd:N #3 + #2 }
-  \hbox_set:Nn #1 {
-    \box_use:N #3
+\cs_new:Nn \__ebproof_append_left:NnN {
+  \__ebproof_shift_x:Nn #1 { \box_wd:c { \__ebproof_box:N #3 } + #2 }
+  \hbox_set:cn { \__ebproof_box:N #1 } {
+    \box_use:c { \__ebproof_box:N #3 }
     \dim_compare:nNnF { #2 } = { 0pt } { \skip_horizontal:n { #2 } }
-    \box_use:N #1
+    \box_use:c { \__ebproof_box:N #1 }
   }
 }
-
-% Shift of two trees to the right so that the axes match. The marks of the one
-% that is shifted are updated accordingly.
-
-\cs_new:Nn \ebproof_align:NN {
+\cs_new:Nn \__ebproof_align:NN {
   \dim_set:Nn \l_tmpa_dim
-    { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #1 {axis} }
+    { \__ebproof_mark:Nn #2 {axis} - \__ebproof_mark:Nn #1 {axis} }
   \dim_compare:nNnTF \l_tmpa_dim < { 0pt } {
-    \ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt }
+    \__ebproof_extend:Nnnnn #2 { -\l_tmpa_dim } { 0pt } { 0pt } { 0pt }
   } {
-    \ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt }
+    \__ebproof_extend:Nnnnn #1 { \l_tmpa_dim } { 0pt } { 0pt } { 0pt }
   }
 }
-
-% Append the contents of the second tree above the first one, with matching
-% axes. The marks of the first tree are preserved.
-
-\cs_new:Nn \ebproof_append_above:NN {
-  \ebproof_align:NN #1 #2
-  \vbox_set:Nn #1 {
-    \box_use:N #2
+\cs_new:Nn \__ebproof_append_above:NN {
+  \__ebproof_align:NN #1 #2
+  \vbox_set:cn  { \__ebproof_box:N #1 } {
+    \box_use:c { \__ebproof_box:N #2 }
     \tex_prevdepth:D -1000pt
-    \box_use:N #1
+    \box_use:c { \__ebproof_box:N #1 }
   }
 }
-
-% Append the contents of the second tree below the first one, with matching
-% axes. The marks of the first tree are preserved.
-
-\cs_new:Nn \ebproof_append_below:NN {
-  \ebproof_align:NN #1 #2
+\cs_new:Nn \__ebproof_append_below:NN {
+  \__ebproof_align:NN #1 #2
   \vbox_set_top:Nn #1 {
-    \box_use:N #1
+    \box_use:c { \__ebproof_box:N #1 }
     \tex_prevdepth:D -1000pt
-    \box_use:N #2
+    \box_use:c { \__ebproof_box:N #2 }
   }
 }
-
-% Shift the material in a tree vertically so that the height and depth are
-% equal (like TeX's \vcenter but around the baseline).
-
-\cs_new:Nn \ebproof_vcenter:N {
-  \dim_set:Nn \l_tmpa_dim { ( \box_ht:N #1 - \box_dp:N #1 ) / 2 }
-  \box_set_eq:NN \l_tmpa_box #1
-  \hbox_set:Nn #1
+\cs_new:Nn \__ebproof_overlay:NN {
+  \__ebproof_align:NN #1 #2
+  \hbox_set:cn { \__ebproof_box:N #1 } {
+    \hbox_overlap_right:n { \box_use:c { \__ebproof_box:N #1 } }
+    \box_use:c { \__ebproof_box:N #2 }
+    \dim_compare:nNnT
+      { \box_wd:c { \__ebproof_box:N #2 } } < { \box_wd:c { \__ebproof_box:N #1 } }
+      { \skip_horizontal:n
+        { \box_wd:c { \__ebproof_box:N #1 } - \box_wd:c { \__ebproof_box:N #2 } } }
+  }
+}
+\cs_new:Nn \__ebproof_vcenter:N {
+  \dim_set:Nn \l_tmpa_dim
+    { ( \box_ht:c { \__ebproof_box:N #1 } - \box_dp:c { \__ebproof_box:N #1 } ) / 2 }
+  \box_set_eq:Nc \l_tmpa_box { \__ebproof_box:N #1 }
+  \hbox_set:cn { \__ebproof_box:N #1 }
     { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_tmpa_box } }
 }
-
-
-%% Making inferences
-%
-% The following commands use the parameters defined at the beginning of the
-% package for actually building proof trees using the commands defined above.
-
-% Append the contents of the second tree above or below the first one,
-% depending on current settings. Axes are aligned and the marks of the first
-% tree are preserved.
-
-\cs_new:Nn \ebproof_append_vertical:NN {
-  \bool_if:NTF \l_ebproof_updown_bool
-    { \ebproof_append_below:NN #1 #2 }
-    { \ebproof_append_above:NN #1 #2 }
-}
-
-% Make a box containing an inference rule with labels, using the current
-% settings. The width and axis position are taken as those of the conclusion
-% of another tree box. The third argument is used as a temporary register for
-% building labels.
-
-\cs_new:Nn \ebproof_make_rule_for:NNN {
-
-  % Build the rule.
-
-  \ebproof_make_vertical:Nnnn #1
-    { \ebproof_mark:Nn #2 {axis} - \ebproof_mark:Nn #2 {left} }
-    { \ebproof_mark:Nn #2 {right} - \ebproof_mark:Nn #2 {left} }
+\cs_new:Nn \__ebproof_append_vertical:NN {
+  \bool_if:NTF \l__ebproof_updown_bool
+    { \__ebproof_append_below:NN #1 #2 }
+    { \__ebproof_append_above:NN #1 #2 }
+}
+\cs_new:Nn \__ebproof_make_rule_for:NNN {
+  \__ebproof_make_vertical:Nnnn #1
+    { \__ebproof_mark:Nn #2 {axis} - \__ebproof_mark:Nn #2 {left} }
+    { \__ebproof_mark:Nn #2 {right} - \__ebproof_mark:Nn #2 {left} }
     {
-      \skip_vertical:N \l_ebproof_rule_margin_dim
-      \tl_if_empty:NF { \l_ebproof_rule_code_tl } {
-        \tl_use:N \l_ebproof_rule_code_tl
-        \skip_vertical:N \l_ebproof_rule_margin_dim
+      \skip_vertical:N \l__ebproof_rule_margin_dim
+      \tl_if_empty:NF { \l__ebproof_rule_code_tl } {
+        \tl_use:N \l__ebproof_rule_code_tl
+        \skip_vertical:N \l__ebproof_rule_margin_dim
       }
     }
-  \ebproof_vcenter:N #1
-
-  % Append the left label
-
-  \tl_if_blank:VF \l_ebproof_left_label_tl {
-    \ebproof_make_simple:Nn #3 {
-      \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n {
-        \cs_set_eq:NN \inserttext \l_ebproof_left_label_tl
-        \tl_use:N \l_ebproof_left_label_template_tl
+  \__ebproof_vcenter:N #1
+  \tl_if_blank:VF \l__ebproof_left_label_tl {
+    \__ebproof_make_simple:Nn #3 {
+      \box_move_down:nn { \l__ebproof_label_axis_dim } { \hbox:n {
+        \cs_set_eq:NN \inserttext \l__ebproof_left_label_tl
+        \tl_use:N \l__ebproof_left_label_template_tl
       } }
     }
-    \box_set_ht:Nn #3 { 0pt }
-    \box_set_dp:Nn #3 { 0pt }
-    \ebproof_append_left:NnN
-      \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box
+    \box_set_ht:cn { \__ebproof_box:N #3 } { 0pt }
+    \box_set_dp:cn { \__ebproof_box:N #3 } { 0pt }
+    \__ebproof_append_left:NnN
+      \l__ebproof_c_box \l__ebproof_label_separation_dim \l__ebproof_d_box
   }
-
-  % Append the right label
-
-  \tl_if_blank:VF \l_ebproof_right_label_tl {
-    \ebproof_make_simple:Nn #3 {
-      \box_move_down:nn { \l_ebproof_label_axis_dim } { \hbox:n {
-        \cs_set_eq:NN \inserttext \l_ebproof_right_label_tl
-        \tl_use:N \l_ebproof_right_label_template_tl
+  \tl_if_blank:VF \l__ebproof_right_label_tl {
+    \__ebproof_make_simple:Nn #3 {
+      \box_move_down:nn { \l__ebproof_label_axis_dim } { \hbox:n {
+        \cs_set_eq:NN \inserttext \l__ebproof_right_label_tl
+        \tl_use:N \l__ebproof_right_label_template_tl
       } }
     }
-    \box_set_ht:Nn #3 { 0pt }
-    \box_set_dp:Nn #3 { 0pt }
-    \ebproof_append_right:NnN
-      \l_ebproof_c_box \l_ebproof_label_separation_dim \l_ebproof_d_box
+    \box_set_ht:cn { \__ebproof_box:N #3 } { 0pt }
+    \box_set_dp:cn { \__ebproof_box:N #3 } { 0pt }
+    \__ebproof_append_right:NnN
+      \l__ebproof_c_box \l__ebproof_label_separation_dim \l__ebproof_d_box
   }
-
-}
-
-
-%% Stack-based interface
-
-%%% The stack
-
-% Logically, box structures are stored on a stack. However, TeX does not
-% provide data structures for that and the grouping mechanism is not flexible
-% enough, so we encode them using what we actually have. A stack for boxes is
-% implemented using a global hbox |\g_ebproof_stack_box| that contains all the
-% boxes successively. A sequence |\g_ebproof_stack_seq| is used to store the
-% dimensions property lists textually. We maintain a counter
-% |\g_ebproof_level_int| with the number of elements on the stack, for
-% consistency checks.
-
-\int_new:N \g_ebproof_level_int
-\box_new:N \g_ebproof_stack_box
-\seq_new:N \g_ebproof_stack_seq
-
-% Clear the stack.
-
-\cs_new:Nn \ebproof_clear_stack: {
-  \int_gset:Nn \g_ebproof_level_int { 0 }
-  \hbox_gset:Nn \g_ebproof_stack_box { }
-  \seq_gclear:N \g_ebproof_stack_seq
-}
-
-% Push the contents of a register on the stack.
-
-\cs_new:Nn \ebproof_push:N {
-  \int_gincr:N \g_ebproof_level_int
-  \hbox_gset:Nn \g_ebproof_stack_box
-    { \hbox_unpack:N \g_ebproof_stack_box \box_use:N #1 }
-  \seq_gput_left:Nv \g_ebproof_stack_seq
-    { l_ebproof_marks_ \__int_value:w #1 _prop }
-}
-
-% Pop the value from the top of the stack into a register.
-
-\cs_new:Nn \ebproof_pop:N {
-  \int_compare:nNnTF { \g_ebproof_level_int } > { 0 } {
-    \int_gdecr:N \g_ebproof_level_int
-    \hbox_gset:Nn \g_ebproof_stack_box {
-      \hbox_unpack:N \g_ebproof_stack_box
+}
+\int_new:N \g__ebproof_level_int
+\box_new:N \g__ebproof_stack_box
+\seq_new:N \g__ebproof_stack_seq
+\cs_new:Nn \__ebproof_clear_stack: {
+  \int_gset:Nn \g__ebproof_level_int { 0 }
+  \hbox_gset:Nn \g__ebproof_stack_box { }
+  \seq_gclear:N \g__ebproof_stack_seq
+}
+\cs_new:Nn \__ebproof_push:N {
+  \int_gincr:N \g__ebproof_level_int
+  \hbox_gset:Nn \g__ebproof_stack_box
+    { \hbox_unpack:N \g__ebproof_stack_box \box_use:c { \__ebproof_box:N #1 } }
+  \seq_gput_left:Nv \g__ebproof_stack_seq
+    { \__ebproof_marks:N #1 }
+}
+\cs_new:Nn \__ebproof_pop:N {
+  \int_compare:nNnTF { \g__ebproof_level_int } > { 0 } {
+    \int_gdecr:N \g__ebproof_level_int
+    \hbox_gset:Nn \g__ebproof_stack_box {
+      \hbox_unpack:N \g__ebproof_stack_box
       \box_gset_to_last:N \g_tmpa_box
     }
-    \box_set_eq_clear:NN #1 \g_tmpa_box
-    \seq_gpop_left:NN \g_ebproof_stack_seq \l_tmpa_tl
-    \tl_set_eq:cN { l_ebproof_marks_ \__int_value:w #1 _prop } \l_tmpa_tl
+    \box_set_eq_clear:cN { \__ebproof_box:N #1 } \g_tmpa_box
+    \seq_gpop_left:NN \g__ebproof_stack_seq \l_tmpa_tl
+    \tl_set_eq:cN { \__ebproof_marks:N #1 } \l_tmpa_tl
   } {
     \PackageError{ebproof}{Missing~premiss~in~a~proof~tree}{}
-    \ebproof_clear:N #1
+    \__ebproof_clear:N #1
   }
 }
-
-%%% Assembling trees
-
-\ebproof_new:N \l_ebproof_a_box
-\ebproof_new:N \l_ebproof_b_box
-\ebproof_new:N \l_ebproof_c_box
-\ebproof_new:N \l_ebproof_d_box
-
-% Join horizontally a number of elements at the top of the stack. If several
-% trees are joined, use the left mark of the left tree, the right mark of the
-% right tree and set the axis in the middle of these marks.
-
-\cs_new:Nn \ebproof_join_horizontal:n {
+\__ebproof_new:N \l__ebproof_a_box
+\__ebproof_new:N \l__ebproof_b_box
+\__ebproof_new:N \l__ebproof_c_box
+\__ebproof_new:N \l__ebproof_d_box
+\cs_new:Nn \__ebproof_join_horizontal:n {
   \int_case:nnF { #1 } {
   { 0 } {
     \group_begin:
-    \ebproof_clear:N \l_ebproof_a_box
-    \ebproof_push:N \l_ebproof_a_box
+    \__ebproof_clear:N \l__ebproof_a_box
+    \__ebproof_push:N \l__ebproof_a_box
     \group_end:
   }
   { 1 } { }
   } {
     \group_begin:
-    \ebproof_pop:N \l_ebproof_a_box
+    \__ebproof_pop:N \l__ebproof_a_box
     \prg_replicate:nn { #1 - 1 } {
-      \ebproof_pop:N \l_ebproof_b_box
-      \ebproof_append_left:NnN
-        \l_ebproof_a_box \l_ebproof_separation_dim \l_ebproof_b_box
+      \__ebproof_pop:N \l__ebproof_b_box
+      \__ebproof_append_left:NnN
+        \l__ebproof_a_box \l__ebproof_separation_dim \l__ebproof_b_box
     }
-    \ebproof_set_mark:Nnn \l_ebproof_a_box { left }
-      { \ebproof_mark:Nn \l_ebproof_b_box { left } }
-    \ebproof_set_mark:Nnn \l_ebproof_a_box { axis }
-      { ( \ebproof_mark:Nn \l_ebproof_a_box { left }
-        + \ebproof_mark:Nn \l_ebproof_a_box { right } ) / 2 }
-    \ebproof_push:N \l_ebproof_a_box
+    \__ebproof_set_mark:Nnn \l__ebproof_a_box { left }
+      { \__ebproof_mark:Nn \l__ebproof_b_box { left } }
+    \__ebproof_set_mark:Nnn \l__ebproof_a_box { axis }
+      { ( \__ebproof_mark:Nn \l__ebproof_a_box { left }
+        + \__ebproof_mark:Nn \l__ebproof_a_box { right } ) / 2 }
+    \__ebproof_push:N \l__ebproof_a_box
     \group_end:
   }
 }
-
-% Join vertically the two elements at the top of the stack, with a horizontal
-% rule of the appropriate size.
-
-\cs_new:Nn \ebproof_join_vertical: {
+\cs_new:Nn \__ebproof_join_vertical: {
   \group_begin:
-  \ebproof_pop:N \l_ebproof_a_box
-  \ebproof_pop:N \l_ebproof_b_box
-  \ebproof_enlarge_conclusion:NN \l_ebproof_b_box \l_ebproof_a_box
-  \ebproof_make_rule_for:NNN \l_ebproof_c_box \l_ebproof_b_box
-    \l_ebproof_d_box
-  \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_c_box
-  \ebproof_append_vertical:NN \l_ebproof_a_box \l_ebproof_b_box
-  \ebproof_push:N \l_ebproof_a_box
+  \__ebproof_pop:N \l__ebproof_a_box
+  \__ebproof_pop:N \l__ebproof_b_box
+  \__ebproof_enlarge_conclusion:NN \l__ebproof_b_box \l__ebproof_a_box
+  \__ebproof_make_rule_for:NNN \l__ebproof_c_box \l__ebproof_b_box
+    \l__ebproof_d_box
+  \__ebproof_append_vertical:NN \l__ebproof_a_box \l__ebproof_c_box
+  \__ebproof_append_vertical:NN \l__ebproof_a_box \l__ebproof_b_box
+  \__ebproof_push:N \l__ebproof_a_box
   \group_end:
 }
-
-%%% High-level commands
-
-% Push a box with default formatting, using explicit alignment if the code
-% contains a |&| character
-
-\cs_new:Npn \ebproof_statement_parse:w #1&#2&#3\ebproof_statement_stop: {
+\cs_new:Npn \__ebproof_statement_parse:w #1 & #2 & #3 \q_stop {
   \tl_if_empty:nTF { #3 } {
-    \ebproof_make_simple:Nn \l_ebproof_a_box
-      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_template_tl }
+    \__ebproof_make_simple:Nn \l__ebproof_a_box
+      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l__ebproof_template_tl }
   } {
-    \ebproof_make_split:Nnn \l_ebproof_a_box
-      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l_ebproof_left_template_tl }
-      { \cs_set:Npn \inserttext { #2 } \tl_use:N \l_ebproof_right_template_tl }
+    \__ebproof_make_split:Nnn \l__ebproof_a_box
+      { \cs_set:Npn \inserttext { #1 } \tl_use:N \l__ebproof_left_template_tl }
+      { \cs_set:Npn \inserttext { #2 } \tl_use:N \l__ebproof_right_template_tl }
   }
-  \ebproof_push:N \l_ebproof_a_box
-}
-
-\cs_new:Nn \ebproof_push_statement:n {
-  \ebproof_statement_parse:w #1&& \ebproof_statement_stop:
-}
-
-
-%% Document interface
-
-%%% Functions to define statements
-
-% The |\g_ebproof_stack_seq| variable contains the list of all defined
-% statements. For each statement |X|, there is a document command |\ebproofX|
-% and the alias |\X| is defined when entering a |prooftree| environment.
-
-\seq_new:N \g_ebproof_statements_seq
-
-% Install the aliases for statements, saving the original value of the control
-% sequences.
-
-\cs_new:Nn \ebproof_setup_statements: {
-  \seq_map_inline:Nn \g_ebproof_statements_seq {
+  \__ebproof_push:N \l__ebproof_a_box
+}
+\cs_new:Nn \__ebproof_push_statement:n {
+  \__ebproof_statement_parse:w #1 & & \q_stop
+}
+\seq_new:N \g__ebproof_statements_seq
+\cs_new:Nn \__ebproof_setup_statements: {
+  \seq_map_inline:Nn \g__ebproof_statements_seq {
     \cs_set_eq:cc { ebproof_saved_ ##1 } { ##1 }
     \cs_set_eq:cc { ##1 } { ebproof ##1 }
   }
 }
-
-% Restore the saved meanings of the control sequences. This is useful when
-% interpreting user-provided code in statement arguments. The meanings are
-% automatically restored when leaving a |prooftree| environment because of
-% grouping.
-
-\cs_new:Nn \ebproof_restore_statements: {
-  \seq_map_inline:Nn \g_ebproof_statements_seq {
+\cs_new:Nn \__ebproof_restore_statements: {
+  \seq_map_inline:Nn \g__ebproof_statements_seq {
     \cs_set_eq:cc { ##1 } { ebproof_saved_ ##1 }
   }
 }
-
-% Define a new statement. The first argument is the name, the second one is an
-% argument specifier as used by |xparse| and the third one is the body of the
-% command.
-
-\cs_new:Nn \ebproof_new_statement:nnn {
+\cs_new:Nn \__ebproof_new_statement:nnn {
   \exp_args:Nc \NewDocumentCommand { ebproof#1 }{ #2 } { #3 }
-  \seq_put_right:Nn \g_ebproof_statements_seq { #1 }
-}
-
-% Define a deprecated statement. The syntax is the same as above except that
-% an extra argument in third position indicates what should be used instead.
-% The effect is the same except that a warning message is issued the first
-% time the statement is used.
-
-\cs_new:Nn \ebproof_new_deprecated_statement:nnnn {
+  \seq_put_right:Nn \g__ebproof_statements_seq { #1 }
+}
+\cs_new:Nn \__ebproof_new_deprecated_statement:nnnn {
   \cs_new:cpn { ebproof_#1_warning: } {
     \PackageWarning { ebproof } { \token_to_str:c{#1}~is~deprecated,~#3 }
     \cs_gset:cn { ebproof_#1_warning: } { }
   }
-  \ebproof_new_statement:nnn { #1 } { #2 }
+  \__ebproof_new_statement:nnn { #1 } { #2 }
     { \use:c { ebproof_#1_warning: } #4 }
 }
-
-
-%%% Basic commands
-
-\ebproof_new_statement:nnn { set } { m } {
+\__ebproof_new_statement:nnn { set } { m } {
   \keys_set:nn { ebproof } { #1 }
 }
-
-\ebproof_new_statement:nnn { hypo } { O{} m } {
+\__ebproof_new_statement:nnn { hypo } { O{} m } {
   \group_begin:
-  \ebproof_restore_statements:
+  \__ebproof_restore_statements:
   \keys_set:nn { ebproof } { #1 }
-  \ebproof_push_statement:n { #2 }
+  \__ebproof_push_statement:n { #2 }
   \group_end:
 }
-
-\ebproof_new_statement:nnn { infer } { O{} m O{} m } {
+\__ebproof_new_statement:nnn { infer } { O{} m O{} m } {
   \group_begin:
-  \ebproof_restore_statements:
+  \__ebproof_restore_statements:
   \keys_set_known:nnN { ebproof / rule~style } { #1 } \l_tmpa_tl
   \keys_set:nV { ebproof } \l_tmpa_tl
-  \tl_set:Nn \l_ebproof_right_label_tl { #3 }
-  \ebproof_join_horizontal:n { #2 }
-  \ebproof_push_statement:n { #4 }
-  \ebproof_join_vertical:
+  \tl_set:Nn \l__ebproof_right_label_tl { #3 }
+  \__ebproof_join_horizontal:n { #2 }
+  \__ebproof_push_statement:n { #4 }
+  \__ebproof_join_vertical:
   \group_end:
 }
-
-\ebproof_new_statement:nnn { ellipsis } { m m } {
+\__ebproof_new_statement:nnn { ellipsis } { m m } {
   \group_begin:
-  \ebproof_restore_statements:
-  \tl_clear:N \l_ebproof_rule_code_tl
-  \ebproof_make_split:Nnn \l_ebproof_a_box { } {
+  \__ebproof_restore_statements:
+  \tl_clear:N \l__ebproof_rule_code_tl
+  \__ebproof_make_split:Nnn \l__ebproof_a_box { } {
     \vbox_set:Nn \l_tmpa_box {
       \skip_vertical:n { 1.2ex }
       \hbox:n { \tex_ignorespaces:D #1 }
@@ -651,117 +428,103 @@ label~axis .dim_set:N = \l_ebproof_label_axis_dim,
     }
     \hbox_overlap_right:n { ~ \box_use:N \l_tmpa_box }
   }
-  \ebproof_push:N \l_ebproof_a_box
-  \ebproof_join_vertical:
-  \ebproof_push_statement:n {#2}
-  \ebproof_join_vertical:
+  \__ebproof_push:N \l__ebproof_a_box
+  \__ebproof_join_vertical:
+  \__ebproof_push_statement:n {#2}
+  \__ebproof_join_vertical:
   \group_end:
 }
-
-
-%%% Modifying trees
-
-% Rewrite the box at the top of the stack while preserving its dimensions an
-% marks. The code is typeset in horizontal mode, with control sequences to
-% access the original box and its marks:
-%  - \treebox is a box register with the original material
-%  - \treemark{NAME} provides the value of a given mark
-
-\ebproof_new_statement:nnn { rewrite } { m } {
+\__ebproof_new_statement:nnn { rewrite } { m } {
   \group_begin:
-  \ebproof_restore_statements:
-  \ebproof_pop:N \l_ebproof_a_box
-  \box_set_eq:NN \l_tmpa_box \l_ebproof_a_box
+  \__ebproof_restore_statements:
+  \__ebproof_pop:N \l__ebproof_a_box
+  \box_set_eq:Nc \l_tmpa_box { \__ebproof_box:N \l__ebproof_a_box }
   \hbox_set:Nn \l_tmpb_box {
     \cs_set_eq:NN \treebox \l_tmpa_box
-    \cs_set:Npn \treemark { \ebproof_mark:Nn \l_ebproof_a_box }
+    \cs_set:Npn \treemark { \__ebproof_mark:Nn \l__ebproof_a_box }
     { #1 }
   }
-  \box_set_wd:Nn \l_tmpb_box { \box_wd:N \l_ebproof_a_box }
-  \box_set_ht:Nn \l_tmpb_box { \box_ht:N \l_ebproof_a_box }
-  \box_set_dp:Nn \l_tmpb_box { \box_dp:N \l_ebproof_a_box }
-  \box_set_eq:NN \l_ebproof_a_box \l_tmpb_box
-  \ebproof_push:N \l_ebproof_a_box
+  \box_set_wd:Nn \l_tmpb_box { \box_wd:c { \__ebproof_box:N \l__ebproof_a_box } }
+  \box_set_ht:Nn \l_tmpb_box { \box_ht:c { \__ebproof_box:N \l__ebproof_a_box } }
+  \box_set_dp:Nn \l_tmpb_box { \box_dp:c { \__ebproof_box:N \l__ebproof_a_box } }
+  \box_set_eq:cN { \__ebproof_box:N \l__ebproof_a_box } \l_tmpb_box
+  \__ebproof_push:N \l__ebproof_a_box
   \group_end:
 }
-
-% Insert |\left| and |\right| delimiters without changing the alignment
-
-\ebproof_new_statement:nnn { delims } { m m } {
+\__ebproof_new_statement:nnn { delims } { m m } {
   \group_begin:
-  \ebproof_restore_statements:
-  \ebproof_pop:N \l_ebproof_a_box
+  \__ebproof_restore_statements:
+  \__ebproof_pop:N \l__ebproof_a_box
   \hbox_set:Nn \l_tmpa_box
-    { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ }
+    { $ \tex_vcenter:D { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } $ }
   \dim_set:Nn \l_tmpa_dim
-    { \box_ht:N \l_tmpa_box - \box_ht:N \l_ebproof_a_box }
-  \hbox_set:Nn \l_ebproof_a_box {
+    { \box_ht:N \l_tmpa_box - \box_ht:c { \__ebproof_box:N \l__ebproof_a_box } }
+  \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } {
     $ #1 \tex_vrule:D
       height \box_ht:N \l_tmpa_box depth \box_dp:N \l_tmpa_box width 0pt
     \tex_right:D . $
   }
-  \ebproof_shift_x:Nn \l_ebproof_a_box { \box_wd:N \l_ebproof_a_box }
-  \hbox_set:Nn \l_ebproof_a_box {
-    \hbox_unpack:N \l_ebproof_a_box
+  \__ebproof_shift_x:Nn \l__ebproof_a_box
+    { \box_wd:c { \__ebproof_box:N \l__ebproof_a_box } }
+  \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box } {
+    \hbox_unpack:c { \__ebproof_box:N \l__ebproof_a_box }
     $ \tex_left:D . \box_use:N \l_tmpa_box #2 $
   }
-  \hbox_set:Nn \l_ebproof_a_box
-    { \box_move_down:nn { \l_tmpa_dim } { \box_use:N \l_ebproof_a_box } }
-  \ebproof_push:N \l_ebproof_a_box
+  \hbox_set:cn { \__ebproof_box:N \l__ebproof_a_box }
+    { \box_move_down:nn { \l_tmpa_dim }
+        { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } }
+  \__ebproof_push:N \l__ebproof_a_box
+  \group_end:
+}
+\__ebproof_new_statement:nnn { overlay } { } {
+  \group_begin:
+  \__ebproof_pop:N \l__ebproof_a_box
+  \__ebproof_pop:N \l__ebproof_b_box
+  \__ebproof_overlay:NN \l__ebproof_a_box \l__ebproof_b_box
+  \__ebproof_push:N \l__ebproof_a_box
   \group_end:
 }
-
-
-%%% Deprecated statements
-
-% These statements were defined in versions 1.x of the package, they are
-% preserved for temporary upwards compatibility and will be removed in a
-% future version.
-
-\ebproof_new_deprecated_statement:nnnn { Alter } { m }
+\__ebproof_new_deprecated_statement:nnnn { Alter } { m }
   { use~\token_to_str:c{rewrite}~instead } { \ebproofrewrite{ #1 \box\treebox } }
-\ebproof_new_deprecated_statement:nnnn { Delims } { }
+\__ebproof_new_deprecated_statement:nnnn { Delims } { }
   { use~\token_to_str:c{delims}~instead } { \ebproofdelims }
-\ebproof_new_deprecated_statement:nnnn { Ellipsis } { }
+\__ebproof_new_deprecated_statement:nnnn { Ellipsis } { }
   { use~\token_to_str:c{ellipsis}~instead } { \ebproofellipsis }
-\ebproof_new_deprecated_statement:nnnn { Hypo } { }
+\__ebproof_new_deprecated_statement:nnnn { Hypo } { }
   { use~\token_to_str:c{hypo}~instead } { \ebproofhypo }
-\ebproof_new_deprecated_statement:nnnn { Infer } { }
+\__ebproof_new_deprecated_statement:nnnn { Infer } { }
   { use~\token_to_str:c{infer}~instead } { \ebproofinfer }
-
-
-%%% Environment interface
-
-\ebproof_clear_stack:
-
-\tl_new:N \l_ebproof_start_level_tl
-
+\__ebproof_clear_stack:
+\tl_new:N \l__ebproof_start_level_tl
 \NewDocumentEnvironment { prooftree } { s O{} } {
+  \group_align_safe_begin:
   \keys_set_known:nnN { ebproof / proof~style } { #2 } \l_tmpa_tl
   \keys_set:nV { ebproof } \l_tmpa_tl
-  \tl_set:Nx \l_ebproof_start_level_tl { \int_use:N \g_ebproof_level_int }
+  \tl_set:Nx \l__ebproof_start_level_tl { \int_use:N \g__ebproof_level_int }
   \vbox_set:Nw \l_tmpa_box
-  \ebproof_setup_statements:
+  \__ebproof_setup_statements:
 } {
   \vbox_set_end:
-  \ebproof_pop:N \l_ebproof_a_box
-  \int_compare:nNnF { \g_ebproof_level_int } = { \tl_use:N \l_ebproof_start_level_tl } {
+  \__ebproof_pop:N \l__ebproof_a_box
+  \int_compare:nNnF { \g__ebproof_level_int } = { \tl_use:N \l__ebproof_start_level_tl } {
     \PackageError{ebproof}{Malformed~proof~tree}{
       Some~hypotheses~were~declared~but~not~used~in~this~tree.}
   }
   \IfBooleanTF { #1 } {
-    \[ \box_use:N \l_ebproof_a_box \]
+    \[ \box_use:c { \__ebproof_box:N \l__ebproof_a_box } \]
     \ignorespacesafterend
   } {
     \hbox_unpack:N \c_empty_box
-    \bool_if:NTF \l_ebproof_center_bool {
-      \hbox:n { $ \tex_vcenter:D { \box_use:N \l_ebproof_a_box } $ }
+    \bool_if:NTF \l__ebproof_center_bool {
+      \hbox:n { $ \tex_vcenter:D { \box_use:c { \__ebproof_box:N \l__ebproof_a_box } } $ }
     } {
-      \box_use:N \l_ebproof_a_box
+      \box_use:c { \__ebproof_box:N \l__ebproof_a_box }
     }
   }
+  \group_align_safe_end:
 }
-
-% A trick for the starred version:
 \cs_new:cpn { prooftree* } { \prooftree* }
 \cs_new:cpn { endprooftree* } { \endprooftree }
+\endinput
+%%
+%% End of file `ebproof.sty'.