diff --git a/docs/iris.sty b/docs/iris.sty
index ba37da23bf89c13efa1fcb24cae746a896b9a645..656e4586166dd9066790b404ae4fc321aba80fad 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}}