diff --git a/algebra/deprecated.v b/algebra/deprecated.v index fe84abfd298e563dd7777a459d371581ff068457..d13f5d786d40e24125b80d63510ef046355b5244 100644 --- a/algebra/deprecated.v +++ b/algebra/deprecated.v @@ -3,4 +3,4 @@ From iris.algebra Require Import ofe. (* Old notation for backwards compatibility. *) (* Deprecated 2016-11-22. Use ofeT instead. *) -Notation cofeT := ofeT. +Notation cofeT := ofeT (only parsing).