deprecated.v 159 Bytes
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1 2 3 4 5 6
From iris.algebra Require Import ofe.

(* Old notation for backwards compatibility. *)

(* Deprecated 2016-11-22. Use ofeT instead. *)
Notation cofeT := ofeT.