From 06b054399131a8b321f0edd046e0fd3b1994af54 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 14 Oct 2016 11:41:09 +0200
Subject: [PATCH] We already have \maybe for the option type
---
docs/iris.sty | 5 -----
1 file changed, 5 deletions(-)
diff --git a/docs/iris.sty b/docs/iris.sty
index ba37da23b..656e45861 100644
--- a/docs/iris.sty
+++ b/docs/iris.sty
@@ -364,11 +364,6 @@
\newcommand{\unittt}{()}
\newcommand{\unit}{1}
-% Option
-\newcommand{\option}[1]{#1^?}
-\newcommand{\Some}{}
-\newcommand{\None}{\textlog{None}}
-
% Agreement
\newcommand{\agm}{\ensuremath{\textmon{Ag}}}
\newcommand{\aginj}{\textlog{ag}}
--
GitLab