From b60fbd73115faac601b2ba8024396c7e85d76df2 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 23 May 2022 12:49:11 +0200
Subject: [PATCH] Revert "Merge branch 'iris_style_improvements' into 'master'"
This reverts commit bfb57e8b8579419ba80b3bcd7004b667675af7da, reversing
changes made to 56e9d264c7ecbebfd209a0048159c12781a8a53d.
Fixes the problem reported at <https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/797#note_81110>
---
tex/iris.sty | 20 ++------------------
1 file changed, 2 insertions(+), 18 deletions(-)
diff --git a/tex/iris.sty b/tex/iris.sty
index 9dbdc4842..7d29b2905 100644
--- a/tex/iris.sty
+++ b/tex/iris.sty
@@ -332,24 +332,8 @@
%% Hoare Triples
-\newcommand*{\hoaresizebox}[1]{%
- \hbox{$\mathsurround=0pt{#1}\mathstrut$}}
-\newcommand*{\hoarescalebox}[2]{%
- \hbox{\scalerel*[1ex]{#1}{#2}}}
-\newcommand{\triple}[5]{%
- \setbox0=\hoaresizebox{{#3}{#5}}%
- \setbox1=\hoarescalebox{#1}{\copy0}%
- \setbox2=\hoarescalebox{#2}{\copy0}%
- \copy1{#3}\copy2%
- \; #4 \;%
- \copy1{#5}\copy2}
-
-\newcommand{\irisbracketgen}[4][]{%
- \setbox0=\hbox{$\mathsurround=0pt{#1}{#4}\mathstrut$}%
- \scalerel*[1ex]{#2}{\copy0}%
- {#4}%
- \scalerel*[1ex]{#3}{\copy0}}
-\newcommand{\curlybracket}[2][]{\irisbracketgen[{#1}]\{\}{#2}}
+% needs extra {...} for some weird reason
+\newcommand{\curlybracket}[1]{{\left\{#1\right\}}}
\NewDocumentCommand \hoare {m m m O{}}{
\curlybracket{#1}\spac #2 \spac \curlybracket{#3}_{#4}%
--
GitLab