diff --git a/algebra/deprecated.v b/algebra/deprecated.v new file mode 100644 index 0000000000000000000000000000000000000000..fe84abfd298e563dd7777a459d371581ff068457 --- /dev/null +++ b/algebra/deprecated.v @@ -0,0 +1,6 @@ +From iris.algebra Require Import ofe. + +(* Old notation for backwards compatibility. *) + +(* Deprecated 2016-11-22. Use ofeT instead. *) +Notation cofeT := ofeT.