From c7240c72617b794a03267d2c6ceba3d0acbdbed0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 10 Oct 2016 17:53:50 +0200
Subject: [PATCH] docs: make Robbert happy, don't use 2 as mnemonic for "to"

---
 docs/iris.sty | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/docs/iris.sty b/docs/iris.sty
index 518651e41..c3bee3ef4 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -323,8 +323,8 @@
 \newcommand{\step}{\ra}
 \newcommand{\lctx}{K}
 
-\newcommand{\toval}{\mathrm{expr2val}}
-\newcommand{\ofval}{\mathrm{val2expr}}
+\newcommand{\toval}{\mathrm{expr\any to\any val}}
+\newcommand{\ofval}{\mathrm{val\any to\any expr}}
 \newcommand{\atomic}{\mathrm{atomic}}
 \newcommand{\red}{\mathrm{red}}
 \newcommand{\Lang}{\Lambda}
-- 
GitLab